Theory TreeToGraphThms

subsection ‹Tree to Graph Theorems›

theory TreeToGraphThms
imports
  IRTreeEvalThms
  IRGraphFrames
  "HOL-Eisbach.Eisbach"
  "HOL-Eisbach.Eisbach_Tools"
begin

subsubsection ‹Extraction and Evaluation of Expression Trees is Deterministic.›

text ‹First, we prove some extra rules that relate each
  type of IRNode to the corresponding IRExpr type that 'rep' will produce.
  These are very helpful for proving that 'rep' is deterministic.
›

named_theorems rep

lemma rep_constant [rep]: 
  "g ⊢ n ≃ e ⟹ 
   kind g n = ConstantNode c ⟹ 
   e = ConstantExpr c"
  by (induction rule: rep.induct; auto)
  
lemma rep_parameter [rep]: 
  "g ⊢ n ≃ e ⟹ 
   kind g n = ParameterNode i ⟹
   (∃s. e = ParameterExpr i s)"
  by (induction rule: rep.induct; auto)

lemma rep_conditional [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = ConditionalNode c t f ⟹
   (∃ ce te fe. e = ConditionalExpr ce te fe)"
  by (induction rule: rep.induct; auto)

lemma rep_abs [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = AbsNode x ⟹
   (∃xe. e = UnaryExpr UnaryAbs xe)"
  by (induction rule: rep.induct; auto)

lemma rep_reverse_bytes [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = ReverseBytesNode x ⟹
   (∃xe. e = UnaryExpr UnaryReverseBytes xe)"
  by (induction rule: rep.induct; auto)

lemma rep_bit_count [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = BitCountNode x ⟹
   (∃xe. e = UnaryExpr UnaryBitCount xe)"
  by (induction rule: rep.induct; auto)

lemma rep_not [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = NotNode x ⟹
   (∃xe. e = UnaryExpr UnaryNot xe)"
  by (induction rule: rep.induct; auto)

lemma rep_negate [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = NegateNode x ⟹
   (∃xe. e = UnaryExpr UnaryNeg xe)"
  by (induction rule: rep.induct; auto)

lemma rep_logicnegation [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = LogicNegationNode x ⟹
   (∃xe. e = UnaryExpr UnaryLogicNegation xe)"
  by (induction rule: rep.induct; auto)

lemma rep_add [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = AddNode x y ⟹
   (∃xe ye. e = BinaryExpr BinAdd xe ye)"
  by (induction rule: rep.induct; auto)

lemma rep_sub [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = SubNode x y ⟹
   (∃xe ye. e = BinaryExpr BinSub xe ye)"
  by (induction rule: rep.induct; auto)

lemma rep_mul [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = MulNode x y ⟹
   (∃xe ye. e = BinaryExpr BinMul xe ye)"
  by (induction rule: rep.induct; auto)

lemma rep_div [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = SignedFloatingIntegerDivNode x y ⟹
   (∃xe ye. e = BinaryExpr BinDiv xe ye)"
  by (induction rule: rep.induct; auto)

lemma rep_mod [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = SignedFloatingIntegerRemNode x y ⟹
   (∃xe ye. e = BinaryExpr BinMod xe ye)"
  by (induction rule: rep.induct; auto)

lemma rep_and [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = AndNode x y ⟹
   (∃xe ye. e = BinaryExpr BinAnd xe ye)"
  by (induction rule: rep.induct; auto)

lemma rep_or [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = OrNode x y ⟹
   (∃xe ye. e = BinaryExpr BinOr xe ye)"
  by (induction rule: rep.induct; auto)

lemma rep_xor [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = XorNode x y ⟹
   (∃xe ye. e = BinaryExpr BinXor xe ye)"
  by (induction rule: rep.induct; auto)

lemma rep_short_circuit_or [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = ShortCircuitOrNode x y ⟹
   (∃xe ye. e = BinaryExpr BinShortCircuitOr xe ye)"
  by (induction rule: rep.induct; auto)

lemma rep_left_shift [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = LeftShiftNode x y ⟹
   (∃xe ye. e = BinaryExpr BinLeftShift xe ye)"
  by (induction rule: rep.induct; auto)

lemma rep_right_shift [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = RightShiftNode x y ⟹
   (∃xe ye. e = BinaryExpr BinRightShift xe ye)"
  by (induction rule: rep.induct; auto)

lemma rep_unsigned_right_shift [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = UnsignedRightShiftNode x y ⟹
   (∃xe ye. e = BinaryExpr BinURightShift xe ye)"
  by (induction rule: rep.induct; auto)

lemma rep_integer_below [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = IntegerBelowNode x y ⟹
   (∃xe ye. e = BinaryExpr BinIntegerBelow xe ye)"
  by (induction rule: rep.induct; auto)

lemma rep_integer_equals [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = IntegerEqualsNode x y ⟹
   (∃xe ye. e = BinaryExpr BinIntegerEquals xe ye)"
  by (induction rule: rep.induct; auto)

lemma rep_integer_less_than [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = IntegerLessThanNode x y ⟹
   (∃xe ye. e = BinaryExpr BinIntegerLessThan xe ye)"
  by (induction rule: rep.induct; auto)

lemma rep_integer_mul_high [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = IntegerMulHighNode x y ⟹
   (∃xe ye. e = BinaryExpr BinIntegerMulHigh xe ye)"
  by (induction rule: rep.induct; auto)

lemma rep_integer_test [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = IntegerTestNode x y ⟹
   (∃xe ye. e = BinaryExpr BinIntegerTest xe ye)"
  by (induction rule: rep.induct; auto)

lemma rep_integer_normalize_compare [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = IntegerNormalizeCompareNode x y ⟹
   (∃xe ye. e = BinaryExpr BinIntegerNormalizeCompare xe ye)"
  by (induction rule: rep.induct; auto)

lemma rep_narrow [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = NarrowNode ib rb x ⟹
   (∃x. e = UnaryExpr (UnaryNarrow ib rb) x)"
  by (induction rule: rep.induct; auto)
 
lemma rep_sign_extend [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = SignExtendNode ib rb x ⟹
   (∃x. e = UnaryExpr (UnarySignExtend ib rb) x)"
  by (induction rule: rep.induct; auto)

lemma rep_zero_extend [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = ZeroExtendNode ib rb x ⟹
   (∃x. e = UnaryExpr (UnaryZeroExtend ib rb) x)"
  by (induction rule: rep.induct; auto)

lemma rep_load_field [rep]:
  "g ⊢ n ≃ e ⟹
   is_preevaluated (kind g n) ⟹
   (∃s. e = LeafExpr n s)"
  by (induction rule: rep.induct; auto)

lemma rep_bytecode_exception [rep]:
  "g ⊢ n ≃ e ⟹
   (kind g n) = BytecodeExceptionNode gu st n' ⟹
   (∃s. e = LeafExpr n s)"
  by (induction rule: rep.induct; auto)

lemma rep_new_array [rep]:
  "g ⊢ n ≃ e ⟹
   (kind g n) = NewArrayNode len st n' ⟹
   (∃s. e = LeafExpr n s)"
  by (induction rule: rep.induct; auto)

lemma rep_array_length [rep]:
  "g ⊢ n ≃ e ⟹
   (kind g n) = ArrayLengthNode x n' ⟹
   (∃s. e = LeafExpr n s)"
  by (induction rule: rep.induct; auto)

lemma rep_load_index [rep]:
  "g ⊢ n ≃ e ⟹
   (kind g n) = LoadIndexedNode index guard x n' ⟹
   (∃s. e = LeafExpr n s)"
  by (induction rule: rep.induct; auto)

lemma rep_store_index [rep]:
  "g ⊢ n ≃ e ⟹
   (kind g n) = StoreIndexedNode check val st index guard x n' ⟹
   (∃s. e = LeafExpr n s)"
  by (induction rule: rep.induct; auto)

lemma rep_ref [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = RefNode n' ⟹
   g ⊢ n' ≃ e"
  by (induction rule: rep.induct; auto)

lemma rep_pi [rep]:
  "g ⊢ n ≃ e ⟹
   kind g n = PiNode n' gu ⟹
   g ⊢ n' ≃ e"
  by (induction rule: rep.induct; auto)

lemma rep_is_null [rep]:
  "g ⊢ n ≃ e ⟹ 
   kind g n = IsNullNode x ⟹ 
   (∃xe. e = (UnaryExpr UnaryIsNull xe))" 
  by (induction rule: rep.induct; auto)

method solve_det uses node =
  (match node in "kind _ _ = node _" for node ⇒ 
    ‹match rep in r: "_ ⟹ _ = node _ ⟹ _" ⇒ 
      ‹match IRNode.inject in i: "(node _ = node _) = _" ⇒
        ‹match RepE in e: "_ ⟹ (⋀x. _ = node x ⟹ _) ⟹ _" ⇒
          ‹match IRNode.distinct in d: "node _ ≠ RefNode _" ⇒
            ‹match IRNode.distinct in f: "node _  ≠ PiNode _ _" ⇒
              ‹metis i e r d f›››››› |
   match node in "kind _ _ = node _ _" for node ⇒ 
    ‹match rep in r: "_ ⟹ _ = node _ _ ⟹ _" ⇒ 
      ‹match IRNode.inject in i: "(node _ _ = node _ _) = _" ⇒
        ‹match RepE in e: "_ ⟹ (⋀x y. _ = node x y ⟹ _) ⟹ _" ⇒
          ‹match IRNode.distinct in d: "node _ _ ≠ RefNode _" ⇒
            ‹match IRNode.distinct in f: "node _ _ ≠ PiNode _ _" ⇒
              ‹metis i e r d f›››››› |
   match node in "kind _ _ = node _ _ _" for node ⇒ 
    ‹match rep in r: "_ ⟹ _ = node _ _ _ ⟹ _" ⇒ 
      ‹match IRNode.inject in i: "(node _ _ _ = node _ _ _) = _" ⇒
        ‹match RepE in e: "_ ⟹ (⋀x y z. _ = node x y z ⟹ _) ⟹ _" ⇒
          ‹match IRNode.distinct in d: "node _ _ _ ≠ RefNode _" ⇒
            ‹match IRNode.distinct in f: "node _ _ _ ≠ PiNode _ _" ⇒
              ‹metis i e r d f›››››› |
  match node in "kind _ _ = node _ _ _" for node ⇒ 
    ‹match rep in r: "_ ⟹ _ = node _ _ _ ⟹ _" ⇒ 
      ‹match IRNode.inject in i: "(node _ _ _ = node _ _ _) = _" ⇒
        ‹match RepE in e: "_ ⟹ (⋀x. _ = node _ _ x ⟹ _) ⟹ _" ⇒
          ‹match IRNode.distinct in d: "node _ _ _ ≠ RefNode _" ⇒
            ‹match IRNode.distinct in f: "node _ _ _ ≠ PiNode _ _" ⇒
              ‹metis i e r d f››››››)

text ‹Now we can prove that 'rep' and 'eval', and their list versions, are deterministic.
›
lemma repDet:
  shows "(g ⊢ n ≃ e⇩1) ⟹ (g ⊢ n ≃ e⇩2) ⟹ e⇩1 = e⇩2"
proof (induction arbitrary: e⇩2 rule: "rep.induct")
  case (ConstantNode n c)
  then show ?case 
    using rep_constant by simp
next
  case (ParameterNode n i s)
  then show ?case
    by (metis IRNode.distinct(3655) IRNode.distinct(3697) ParameterNodeE rep_parameter)
next
  case (ConditionalNode n c t f ce te fe)
  then show ?case
    by (metis ConditionalNodeE IRNode.distinct(925) IRNode.distinct(967) IRNode.sel(90) IRNode.sel(93) IRNode.sel(94) rep_conditional)
next
  case (AbsNode n x xe)
  then show ?case
    by (solve_det node: AbsNode)
next
  case (ReverseBytesNode n x xe)
  then show ?case
    by (solve_det node: ReverseBytesNode)
next
  case (BitCountNode n x xe)
  then show ?case
    by (solve_det node: BitCountNode)
next
  case (NotNode n x xe)
  then show ?case
    by (solve_det node: NotNode)
next
  case (NegateNode n x xe)
  then show ?case
    by (solve_det node: NegateNode)
next
  case (LogicNegationNode n x xe)
  then show ?case
    by (solve_det node: LogicNegationNode)
next
  case (AddNode n x y xe ye)
  then show ?case
    by (solve_det node: AddNode)
next
  case (MulNode n x y xe ye)
  then show ?case
    by (solve_det node: MulNode)
next
  case (DivNode n x y xe ye)
  then show ?case
    by (solve_det node: DivNode)
next
  case (ModNode n x y xe ye)
  then show ?case
    by (solve_det node: ModNode)
next
  case (SubNode n x y xe ye)
  then show ?case
    by (solve_det node: SubNode)
next
  case (AndNode n x y xe ye)
  then show ?case
    by (solve_det node: AndNode)
next
  case (OrNode n x y xe ye)
  then show ?case
    by (solve_det node: OrNode)
next
  case (XorNode n x y xe ye)
  then show ?case
    by (solve_det node: XorNode)
next
  case (ShortCircuitOrNode n x y xe ye)
  then show ?case
    by (solve_det node: ShortCircuitOrNode)
next
  case (LeftShiftNode n x y xe ye)
  then show ?case
    by (solve_det node: LeftShiftNode)
next
  case (RightShiftNode n x y xe ye)
  then show ?case
    by (solve_det node: RightShiftNode)
next
  case (UnsignedRightShiftNode n x y xe ye)
  then show ?case
    by (solve_det node: UnsignedRightShiftNode)
next
  case (IntegerBelowNode n x y xe ye)
  then show ?case
    by (solve_det node: IntegerBelowNode)
next
  case (IntegerEqualsNode n x y xe ye)
  then show ?case
    by (solve_det node: IntegerEqualsNode)
next
  case (IntegerLessThanNode n x y xe ye)
  then show ?case
    by (solve_det node: IntegerLessThanNode)
next
  case (IntegerTestNode n x y xe ye)
  then show ?case
    by (solve_det node: IntegerTestNode)
next
  case (IntegerNormalizeCompareNode n x y xe ye)
  then show ?case
    by (solve_det node: IntegerNormalizeCompareNode)
next
  case (IntegerMulHighNode n x xe)
  then show ?case
    by (solve_det node: IntegerMulHighNode)
next
  case (NarrowNode n x xe)
  then show ?case
    using NarrowNodeE rep_narrow
    by (metis IRNode.distinct(3361) IRNode.distinct(3403) IRNode.inject(36))
next
  case (SignExtendNode n x xe)
  then show ?case
    using SignExtendNodeE rep_sign_extend
    by (metis IRNode.distinct(3707) IRNode.distinct(3919) IRNode.inject(48))
next
  case (ZeroExtendNode n x xe)
  then show ?case
    using ZeroExtendNodeE rep_zero_extend
    by (metis IRNode.distinct(3735) IRNode.distinct(4157) IRNode.inject(62))
next
  case (LeafNode n s)
  then show ?case
    using rep_load_field LeafNodeE
    by (metis is_preevaluated.simps(48) is_preevaluated.simps(65))
next
  case (RefNode n')
  then show ?case
    using rep_ref by blast
next
  case (PiNode n v)
  then show ?case
    using rep_pi by blast
next
  case (IsNullNode n v)
  then show ?case
    using IsNullNodeE rep_is_null
    by (metis IRNode.distinct(2557) IRNode.distinct(2599) IRNode.inject(24))
qed

lemma repAllDet:
  "g ⊢ xs [≃] e1 ⟹
   g ⊢ xs [≃] e2 ⟹
   e1 = e2"
proof (induction arbitrary: e2 rule: "replist.induct")
  case RepNil
  then show ?case
    using replist.cases by auto 
next
  case (RepCons x xe xs xse)
  then show ?case
    by (metis list.distinct(1) list.sel(1,3) repDet replist.cases) 
qed

lemma encodeEvalDet:
  "[g,m,p] ⊢ e ↦ v1 ⟹ 
   [g,m,p] ⊢ e ↦ v2 ⟹
   v1 = v2"
  by (metis encodeeval.simps evalDet repDet)

lemma graphDet: "([g,m,p] ⊢ n ↦ v⇩1) ∧ ([g,m,p] ⊢ n ↦ v⇩2) ⟹ v⇩1 = v⇩2"
  by (auto simp add: encodeEvalDet)

lemma encodeEvalAllDet:
  "[g, m, p] ⊢ nids [↦] vs ⟹ [g, m, p] ⊢ nids [↦] vs' ⟹ vs = vs'"
  using repAllDet evalAllDet
  by (metis encodeEvalAll.simps)

subsubsection ‹Monotonicity of Graph Refinement›

text ‹
Lift refinement monotonicity to graph level.
Hopefully these shouldn't really be required.
›

lemma mono_abs:
  assumes "kind g1 n = AbsNode x ∧ kind g2 n = AbsNode x"
  assumes "(g1 ⊢ x ≃ xe1) ∧ (g2 ⊢ x ≃ xe2)"
  assumes "xe1 ≥ xe2"
  assumes "(g1 ⊢ n ≃ e1) ∧ (g2 ⊢ n ≃ e2)"
  shows "e1 ≥ e2"
  by (metis AbsNode assms mono_unary repDet)

lemma mono_not:
  assumes "kind g1 n = NotNode x ∧ kind g2 n = NotNode x"
  assumes "(g1 ⊢ x ≃ xe1) ∧ (g2 ⊢ x ≃ xe2)"
  assumes "xe1 ≥ xe2"
  assumes "(g1 ⊢ n ≃ e1) ∧ (g2 ⊢ n ≃ e2)"
  shows "e1 ≥ e2"
  by (metis NotNode assms mono_unary repDet)

lemma mono_negate:
  assumes "kind g1 n = NegateNode x ∧ kind g2 n = NegateNode x"
  assumes "(g1 ⊢ x ≃ xe1) ∧ (g2 ⊢ x ≃ xe2)"
  assumes "xe1 ≥ xe2"
  assumes "(g1 ⊢ n ≃ e1) ∧ (g2 ⊢ n ≃ e2)"
  shows "e1 ≥ e2"
  by (metis NegateNode assms mono_unary repDet)

lemma mono_logic_negation:
  assumes "kind g1 n = LogicNegationNode x ∧ kind g2 n = LogicNegationNode x"
  assumes "(g1 ⊢ x ≃ xe1) ∧ (g2 ⊢ x ≃ xe2)"
  assumes "xe1 ≥ xe2"
  assumes "(g1 ⊢ n ≃ e1) ∧ (g2 ⊢ n ≃ e2)"
  shows "e1 ≥ e2"
  by (metis LogicNegationNode assms mono_unary repDet)

lemma mono_narrow:
  assumes "kind g1 n = NarrowNode ib rb x ∧ kind g2 n = NarrowNode ib rb x"
  assumes "(g1 ⊢ x ≃ xe1) ∧ (g2 ⊢ x ≃ xe2)"
  assumes "xe1 ≥ xe2"
  assumes "(g1 ⊢ n ≃ e1) ∧ (g2 ⊢ n ≃ e2)"
  shows "e1 ≥ e2"
  by (metis NarrowNode assms mono_unary repDet)

lemma mono_sign_extend:
  assumes "kind g1 n = SignExtendNode ib rb x ∧ kind g2 n = SignExtendNode ib rb x"
  assumes "(g1 ⊢ x ≃ xe1) ∧ (g2 ⊢ x ≃ xe2)"
  assumes "xe1 ≥ xe2"
  assumes "(g1 ⊢ n ≃ e1) ∧ (g2 ⊢ n ≃ e2)"
  shows "e1 ≥ e2"
  by (metis SignExtendNode assms mono_unary repDet)

lemma mono_zero_extend:
  assumes "kind g1 n = ZeroExtendNode ib rb x ∧ kind g2 n = ZeroExtendNode ib rb x"
  assumes "(g1 ⊢ x ≃ xe1) ∧ (g2 ⊢ x ≃ xe2)"
  assumes "xe1 ≥ xe2"
  assumes "(g1 ⊢ n ≃ e1) ∧ (g2 ⊢ n ≃ e2)"
  shows "e1 ≥ e2"
  by (metis ZeroExtendNode assms mono_unary repDet)

lemma mono_conditional_graph:
  assumes "kind g1 n = ConditionalNode c t f ∧ kind g2 n = ConditionalNode c t f"
  assumes "(g1 ⊢ c ≃ ce1) ∧ (g2 ⊢ c ≃ ce2)"
  assumes "(g1 ⊢ t ≃ te1) ∧ (g2 ⊢ t ≃ te2)"
  assumes "(g1 ⊢ f ≃ fe1) ∧ (g2 ⊢ f ≃ fe2)"
  assumes "ce1 ≥ ce2 ∧ te1 ≥ te2 ∧ fe1 ≥ fe2"
  assumes "(g1 ⊢ n ≃ e1) ∧ (g2 ⊢ n ≃ e2)"
  shows "e1 ≥ e2"
  by (smt (verit, ccfv_SIG) ConditionalNode assms mono_conditional repDet le_expr_def)

lemma mono_add:
  assumes "kind g1 n = AddNode x y ∧ kind g2 n = AddNode x y"
  assumes "(g1 ⊢ x ≃ xe1) ∧ (g2 ⊢ x ≃ xe2)"
  assumes "(g1 ⊢ y ≃ ye1) ∧ (g2 ⊢ y ≃ ye2)"
  assumes "xe1 ≥ xe2 ∧ ye1 ≥ ye2"
  assumes "(g1 ⊢ n ≃ e1) ∧ (g2 ⊢ n ≃ e2)"
  shows "e1 ≥ e2"
  by (metis (no_types, lifting) AddNode mono_binary assms repDet)

lemma mono_mul:
  assumes "kind g1 n = MulNode x y ∧ kind g2 n = MulNode x y"
  assumes "(g1 ⊢ x ≃ xe1) ∧ (g2 ⊢ x ≃ xe2)"
  assumes "(g1 ⊢ y ≃ ye1) ∧ (g2 ⊢ y ≃ ye2)"
  assumes "xe1 ≥ xe2 ∧ ye1 ≥ ye2"
  assumes "(g1 ⊢ n ≃ e1) ∧ (g2 ⊢ n ≃ e2)"
  shows "e1 ≥ e2"
  by (metis (no_types, lifting) MulNode assms mono_binary repDet)

lemma mono_div:
  assumes "kind g1 n = SignedFloatingIntegerDivNode x y ∧ kind g2 n = SignedFloatingIntegerDivNode x y"
  assumes "(g1 ⊢ x ≃ xe1) ∧ (g2 ⊢ x ≃ xe2)"
  assumes "(g1 ⊢ y ≃ ye1) ∧ (g2 ⊢ y ≃ ye2)"
  assumes "xe1 ≥ xe2 ∧ ye1 ≥ ye2"
  assumes "(g1 ⊢ n ≃ e1) ∧ (g2 ⊢ n ≃ e2)"
  shows "e1 ≥ e2"
  by (metis (no_types, lifting) DivNode assms mono_binary repDet)

lemma mono_mod:
  assumes "kind g1 n = SignedFloatingIntegerRemNode x y ∧ kind g2 n = SignedFloatingIntegerRemNode x y"
  assumes "(g1 ⊢ x ≃ xe1) ∧ (g2 ⊢ x ≃ xe2)"
  assumes "(g1 ⊢ y ≃ ye1) ∧ (g2 ⊢ y ≃ ye2)"
  assumes "xe1 ≥ xe2 ∧ ye1 ≥ ye2"
  assumes "(g1 ⊢ n ≃ e1) ∧ (g2 ⊢ n ≃ e2)"
  shows "e1 ≥ e2"
  by (metis (no_types, lifting) ModNode assms mono_binary repDet)

lemma term_graph_evaluation:
  "(g ⊢ n ⊴ e) ⟹ (∀ m p v . ([m,p] ⊢ e ↦ v) ⟶ ([g,m,p] ⊢ n ↦ v))"
  using graph_represents_expression_def encodeeval.simps by (auto; meson)

lemma encodes_contains:
  "g ⊢ n ≃ e ⟹
  kind g n ≠ NoNode"
  apply (induction rule: rep.induct)
  apply (match IRNode.distinct in e: "?n ≠ NoNode" ⇒ ‹presburger add: e›)+
  by fastforce+

lemma no_encoding:
  assumes "n ∉ ids g"
  shows "¬(g ⊢ n ≃ e)"
  using assms apply simp apply (rule notI) by (induction e; simp add: encodes_contains)

lemma not_excluded_keep_type:
  assumes "n ∈ ids g1"
  assumes "n ∉ excluded"
  assumes "(excluded ⊴ as_set g1) ⊆ as_set g2"
  shows "kind g1 n = kind g2 n ∧ stamp g1 n = stamp g2 n"
  using assms by (auto simp add: domain_subtraction_def as_set_def)

method metis_node_eq_unary for node :: "'a ⇒ IRNode" =
  (match IRNode.inject in i: "(node _ = node _) = _" ⇒ 
      ‹metis i›)
method metis_node_eq_binary for node :: "'a ⇒ 'a ⇒ IRNode" =
  (match IRNode.inject in i: "(node _ _ = node _ _) = _" ⇒ 
      ‹metis i›)
method metis_node_eq_ternary for node :: "'a ⇒ 'a ⇒ 'a ⇒ IRNode" =
  (match IRNode.inject in i: "(node _ _ _ = node _ _ _) = _" ⇒ 
      ‹metis i›)

subsubsection ‹Lift Data-flow Tree Refinement to Graph Refinement›

theorem graph_semantics_preservation:
  assumes a: "e1' ≥ e2'"
  assumes b: "({n'} ⊴ as_set g1) ⊆ as_set g2"
  assumes c: "g1 ⊢ n' ≃ e1'"
  assumes d: "g2 ⊢ n' ≃ e2'"
  shows "graph_refinement g1 g2"
  unfolding graph_refinement_def apply rule
  apply (metis b d ids_some no_encoding not_excluded_keep_type singleton_iff subsetI)
  apply (rule allI) apply (rule impI) apply (rule allI) apply (rule impI)
  unfolding graph_represents_expression_def
proof -
  fix n e1
  assume e: "n ∈ ids g1"
  assume f: "(g1 ⊢ n ≃ e1)"
  show "∃ e2. (g2 ⊢ n ≃ e2) ∧ e1 ≥ e2"
  proof (cases "n = n'")
    case True
    have g: "e1 = e1'" 
      using f by (simp add: repDet True c)
    have h: "(g2 ⊢ n ≃ e2') ∧ e1' ≥ e2'"
      using a by (simp add: d True)
    then show ?thesis 
      by (auto simp add: g)
  next
    case False
    have "n ∉ {n'}"
      by (simp add: False)
    then have i: "kind g1 n = kind g2 n ∧ stamp g1 n = stamp g2 n"
      using not_excluded_keep_type b e by presburger
    show ?thesis 
      using f i
    proof (induction e1)
      case (ConstantNode n c)
      then show ?case
        by (metis eq_refl rep.ConstantNode)
    next
      case (ParameterNode n i s)
      then show ?case
        by (metis eq_refl rep.ParameterNode)
    next
      case (ConditionalNode n c t f ce1 te1 fe1)
      have k: "g1 ⊢ n ≃ ConditionalExpr ce1 te1 fe1" 
        using ConditionalNode by (simp add: ConditionalNode.hyps(2) rep.ConditionalNode f)
      obtain cn tn fn where l: "kind g1 n = ConditionalNode cn tn fn"
        by (auto simp add: ConditionalNode.hyps(1))
      then have mc: "g1 ⊢ cn ≃ ce1"
        using ConditionalNode.hyps(1,2) by simp
      from l have mt: "g1 ⊢ tn ≃ te1"
        using ConditionalNode.hyps(1,3) by simp
      from l have mf: "g1 ⊢ fn ≃ fe1"
        using ConditionalNode.hyps(1,4) by simp
      then show ?case
      proof -
        have "g1 ⊢ cn ≃ ce1" 
          by (simp add: mc)
        have "g1 ⊢ tn ≃ te1" 
          by (simp add: mt)
        have "g1 ⊢ fn ≃ fe1" 
          by (simp add: mf)
        have cer: "∃ ce2. (g2 ⊢ cn ≃ ce2) ∧ ce1 ≥ ce2"
          using ConditionalNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_ternary ConditionalNode)
        have ter: "∃ te2. (g2 ⊢ tn ≃ te2) ∧ te1 ≥ te2"
          using ConditionalNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_ternary ConditionalNode)
        have "∃ fe2. (g2 ⊢ fn ≃ fe2) ∧ fe1 ≥ fe2"
          using ConditionalNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_ternary ConditionalNode)
        then have "∃ ce2 te2 fe2. (g2 ⊢ n ≃ ConditionalExpr ce2 te2 fe2) ∧ 
               ConditionalExpr ce1 te1 fe1 ≥ ConditionalExpr ce2 te2 fe2"
          apply meson
          by (smt (verit, best) mono_conditional ConditionalNode.prems l rep.ConditionalNode cer ter)
        then show ?thesis
          by meson
      qed
    next
      case (AbsNode n x xe1)
      have k: "g1 ⊢ n ≃ UnaryExpr UnaryAbs xe1" 
        using AbsNode by (simp add: AbsNode.hyps(2) rep.AbsNode f)
      obtain xn where l: "kind g1 n = AbsNode xn"
        by (auto simp add: AbsNode.hyps(1))
      then have m: "g1 ⊢ xn ≃ xe1"
        using AbsNode.hyps(1,2) by simp
      then show ?case
      proof (cases "xn = n'")
        case True
        then have n: "xe1 = e1'" 
          using m by (simp add: repDet c)
        then have ev: "g2 ⊢ n ≃ UnaryExpr UnaryAbs e2'" 
          using l d by (simp add: rep.AbsNode True AbsNode.prems)
        then have r: "UnaryExpr UnaryAbs e1' ≥ UnaryExpr UnaryAbs e2'"
          by (meson a mono_unary)
        then show ?thesis
          by (metis n ev)
      next
        case False
        have "g1 ⊢ xn ≃ xe1" 
          by (simp add: m)
        have "∃ xe2. (g2 ⊢ xn ≃ xe2) ∧ xe1 ≥ xe2"
          using AbsNode False b encodes_contains l not_excluded_keep_type not_in_g singleton_iff
          by (metis_node_eq_unary AbsNode)
        then have "∃ xe2. (g2 ⊢ n ≃ UnaryExpr UnaryAbs xe2) ∧ 
           UnaryExpr UnaryAbs xe1 ≥ UnaryExpr UnaryAbs xe2"
          by (metis AbsNode.prems l mono_unary rep.AbsNode)
        then show ?thesis
          by meson
      qed
    next
      case (ReverseBytesNode n x xe1)
      have k: "g1 ⊢ n ≃ UnaryExpr UnaryReverseBytes xe1"
        by (simp add: ReverseBytesNode.hyps(1,2) rep.ReverseBytesNode)
      obtain xn where l: "kind g1 n = ReverseBytesNode xn"
        by (simp add: ReverseBytesNode.hyps(1))
      then have m: "g1 ⊢ xn ≃ xe1"
        by (metis IRNode.inject(45) ReverseBytesNode.hyps(1,2))
      then show ?case
      proof (cases "xn = n'")
        case True
        then have n: "xe1 = e1'"
          using m by (simp add: repDet c)
        then have ev: "g2 ⊢ n ≃ UnaryExpr UnaryReverseBytes e2'"
          using ReverseBytesNode.prems True d l rep.ReverseBytesNode by presburger
        then have r: "UnaryExpr UnaryReverseBytes e1' ≥ UnaryExpr UnaryReverseBytes e2'"
          by (meson a mono_unary)
        then show ?thesis
          by (metis n ev)
      next
        case False
        have "g1 ⊢ xn ≃ xe1"
          by (simp add: m)
        have "∃ xe2. (g2 ⊢ xn ≃ xe2) ∧ xe1 ≥ xe2"
          by (metis False IRNode.inject(45) ReverseBytesNode.IH ReverseBytesNode.hyps(1,2) b l
              encodes_contains ids_some not_excluded_keep_type singleton_iff)
        then have "∃ xe2. (g2 ⊢ n ≃ UnaryExpr UnaryReverseBytes xe2) ∧
  UnaryExpr UnaryReverseBytes xe1 ≥ UnaryExpr UnaryReverseBytes xe2"
          by (metis ReverseBytesNode.prems l mono_unary rep.ReverseBytesNode)
        then show ?thesis
          by meson
      qed
    next
      case (BitCountNode n x xe1)
      have k: "g1 ⊢ n ≃ UnaryExpr UnaryBitCount xe1"
        by (simp add: BitCountNode.hyps(1,2) rep.BitCountNode)
      obtain xn where l: "kind g1 n = BitCountNode xn"
        by (simp add: BitCountNode.hyps(1))
      then have m: "g1 ⊢ xn ≃ xe1"
        by (metis BitCountNode.hyps(1,2) IRNode.inject(6))
      then show ?case
      proof (cases "xn = n'")
        case True
        then have n: "xe1 = e1'"
          using m by (simp add: repDet c)
        then have ev: "g2 ⊢ n ≃ UnaryExpr UnaryBitCount e2'"
          using BitCountNode.prems True d l rep.BitCountNode by presburger
        then have r: "UnaryExpr UnaryBitCount e1' ≥ UnaryExpr UnaryBitCount e2'"
          by (meson a mono_unary)
        then show ?thesis
          by (metis n ev)
      next
        case False
        have "g1 ⊢ xn ≃ xe1"
          by (simp add: m)
        have "∃ xe2. (g2 ⊢ xn ≃ xe2) ∧ xe1 ≥ xe2"
          by (metis BitCountNode.IH BitCountNode.hyps(1) False IRNode.inject(6) b emptyE insertE l m
              no_encoding not_excluded_keep_type)
        then have "∃ xe2. (g2 ⊢ n ≃ UnaryExpr UnaryBitCount xe2) ∧
      UnaryExpr UnaryBitCount xe1 ≥ UnaryExpr UnaryBitCount xe2"
          by (metis BitCountNode.prems l mono_unary rep.BitCountNode)
        then show ?thesis
          by meson
      qed
    next
      case (NotNode n x xe1)
      have k: "g1 ⊢ n ≃ UnaryExpr UnaryNot xe1" 
        using NotNode by (simp add: NotNode.hyps(2) rep.NotNode f)
      obtain xn where l: "kind g1 n = NotNode xn"
        by (auto simp add: NotNode.hyps(1))
      then have m: "g1 ⊢ xn ≃ xe1"
        using NotNode.hyps(1,2) by simp
      then show ?case
      proof (cases "xn = n'")
        case True
        then have n: "xe1 = e1'" 
          using m by (simp add: repDet c)
        then have ev: "g2 ⊢ n ≃ UnaryExpr UnaryNot e2'" 
          using l by (simp add: rep.NotNode d True NotNode.prems)
        then have r: "UnaryExpr UnaryNot e1' ≥ UnaryExpr UnaryNot e2'"
          by (meson a mono_unary)
        then show ?thesis
          by (metis n ev)
      next
        case False
        have "g1 ⊢ xn ≃ xe1" 
          by (simp add: m)
        have "∃ xe2. (g2 ⊢ xn ≃ xe2) ∧ xe1 ≥ xe2"
          using NotNode False b l not_excluded_keep_type singletonD no_encoding
          by (metis_node_eq_unary NotNode)
        then have "∃ xe2. (g2 ⊢ n ≃ UnaryExpr UnaryNot xe2) ∧ 
           UnaryExpr UnaryNot xe1 ≥ UnaryExpr UnaryNot xe2"
          by (metis NotNode.prems l mono_unary rep.NotNode)
        then show ?thesis
          by meson
      qed
    next
      case (NegateNode n x xe1)
      have k: "g1 ⊢ n ≃ UnaryExpr UnaryNeg xe1" 
        using NegateNode by (simp add: NegateNode.hyps(2) rep.NegateNode f)
      obtain xn where l: "kind g1 n = NegateNode xn"
        by (auto simp add: NegateNode.hyps(1))
      then have m: "g1 ⊢ xn ≃ xe1"
        using NegateNode.hyps(1,2) by simp
      then show ?case
      proof (cases "xn = n'")
        case True
        then have n: "xe1 = e1'" 
          using m by (simp add: c repDet)
        then have ev: "g2 ⊢ n ≃ UnaryExpr UnaryNeg e2'" 
          using l by (simp add: rep.NegateNode True NegateNode.prems d)
        then have r: "UnaryExpr UnaryNeg e1' ≥ UnaryExpr UnaryNeg e2'"
          by (meson a mono_unary)
        then show ?thesis
          by (metis n ev)
      next
        case False
        have "g1 ⊢ xn ≃ xe1" 
          by (simp add: m)
        have "∃ xe2. (g2 ⊢ xn ≃ xe2) ∧ xe1 ≥ xe2"
          using NegateNode False b l not_excluded_keep_type singletonD no_encoding
          by (metis_node_eq_unary NegateNode)
        then have "∃ xe2. (g2 ⊢ n ≃ UnaryExpr UnaryNeg xe2) ∧ 
           UnaryExpr UnaryNeg xe1 ≥ UnaryExpr UnaryNeg xe2"
          by (metis NegateNode.prems l mono_unary rep.NegateNode)
        then show ?thesis
          by meson
      qed
    next
      case (LogicNegationNode n x xe1)
      have k: "g1 ⊢ n ≃ UnaryExpr UnaryLogicNegation xe1" 
        using LogicNegationNode by (simp add: LogicNegationNode.hyps(2) rep.LogicNegationNode)
      obtain xn where l: "kind g1 n = LogicNegationNode xn"
        by (simp add: LogicNegationNode.hyps(1))
      then have m: "g1 ⊢ xn ≃ xe1"
        using LogicNegationNode.hyps(1,2) by simp
      then show ?case
      proof (cases "xn = n'")
        case True
        then have n: "xe1 = e1'" 
          using m by (simp add: c repDet)
        then have ev: "g2 ⊢ n ≃ UnaryExpr UnaryLogicNegation e2'" 
          using l by (simp add: rep.LogicNegationNode True LogicNegationNode.prems d
                                LogicNegationNode.hyps(1))
        then have r: "UnaryExpr UnaryLogicNegation e1' ≥ UnaryExpr UnaryLogicNegation e2'"
          by (meson a mono_unary)
        then show ?thesis
          by (metis n ev)
      next
        case False
        have "g1 ⊢ xn ≃ xe1" 
          by (simp add: m)
        have "∃ xe2. (g2 ⊢ xn ≃ xe2) ∧ xe1 ≥ xe2"
          using LogicNegationNode False b l not_excluded_keep_type singletonD no_encoding
          by (metis_node_eq_unary LogicNegationNode)
        then have "∃ xe2. (g2 ⊢ n ≃ UnaryExpr UnaryLogicNegation xe2) ∧ 
 UnaryExpr UnaryLogicNegation xe1 ≥ UnaryExpr UnaryLogicNegation xe2"
          by (metis LogicNegationNode.prems l mono_unary rep.LogicNegationNode)
        then show ?thesis
          by meson
      qed
    next
      case (AddNode n x y xe1 ye1)
      have k: "g1 ⊢ n ≃ BinaryExpr BinAdd xe1 ye1" 
        using AddNode by (simp add: AddNode.hyps(2) rep.AddNode f)
      obtain xn yn where l: "kind g1 n = AddNode xn yn"
        by (simp add: AddNode.hyps(1))
      then have mx: "g1 ⊢ xn ≃ xe1"
        using AddNode.hyps(1,2) by simp
      from l have my: "g1 ⊢ yn ≃ ye1"
        using AddNode.hyps(1,3) by simp
      then show ?case
      proof -
        have "g1 ⊢ xn ≃ xe1" 
          by (simp add: mx)
        have "g1 ⊢ yn ≃ ye1" 
          by (simp add: my)
        have xer: "∃ xe2. (g2 ⊢ xn ≃ xe2) ∧ xe1 ≥ xe2"
          using AddNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_binary AddNode)
        have "∃ ye2. (g2 ⊢ yn ≃ ye2) ∧ ye1 ≥ ye2"
          using AddNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_binary AddNode)
        then have "∃ xe2 ye2. (g2 ⊢ n ≃ BinaryExpr BinAdd xe2 ye2) ∧ 
            BinaryExpr BinAdd xe1 ye1 ≥ BinaryExpr BinAdd xe2 ye2"
          by (metis AddNode.prems l mono_binary rep.AddNode xer)
        then show ?thesis
          by meson
      qed
    next
      case (MulNode n x y xe1 ye1)
      have k: "g1 ⊢ n ≃ BinaryExpr BinMul xe1 ye1" 
        using MulNode by (simp add: MulNode.hyps(2) rep.MulNode f)
      obtain xn yn where l: "kind g1 n = MulNode xn yn"
        by (simp add: MulNode.hyps(1))
      then have mx: "g1 ⊢ xn ≃ xe1"
        using MulNode.hyps(1,2) by simp
      from l have my: "g1 ⊢ yn ≃ ye1"
        using MulNode.hyps(1,3) by simp
      then show ?case
      proof -
        have "g1 ⊢ xn ≃ xe1" 
          by (simp add: mx)
        have "g1 ⊢ yn ≃ ye1" 
          by (simp add: my)
        have xer: "∃ xe2. (g2 ⊢ xn ≃ xe2) ∧ xe1 ≥ xe2"
          using MulNode  a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_binary MulNode)
        have "∃ ye2. (g2 ⊢ yn ≃ ye2) ∧ ye1 ≥ ye2"
          using MulNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_binary MulNode)
        then have "∃ xe2 ye2. (g2 ⊢ n ≃ BinaryExpr BinMul xe2 ye2) ∧ 
            BinaryExpr BinMul xe1 ye1 ≥ BinaryExpr BinMul xe2 ye2"
          by (metis MulNode.prems l mono_binary rep.MulNode xer)
        then show ?thesis
          by meson
      qed
    next
      case (DivNode n x y xe1 ye1)
      have k: "g1 ⊢ n ≃ BinaryExpr BinDiv xe1 ye1" 
        using DivNode by (simp add: DivNode.hyps(2) rep.DivNode f)
      obtain xn yn where l: "kind g1 n = SignedFloatingIntegerDivNode xn yn"
        by (simp add: DivNode.hyps(1))
      then have mx: "g1 ⊢ xn ≃ xe1"
        using DivNode.hyps(1,2) by simp
      from l have my: "g1 ⊢ yn ≃ ye1"
        using DivNode.hyps(1,3) by simp
      then show ?case
      proof -
        have "g1 ⊢ xn ≃ xe1" 
          by (simp add: mx)
        have "g1 ⊢ yn ≃ ye1" 
          by (simp add: my)
        have xer: "∃ xe2. (g2 ⊢ xn ≃ xe2) ∧ xe1 ≥ xe2"
          using DivNode  a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_binary SignedFloatingIntegerDivNode)
        have "∃ ye2. (g2 ⊢ yn ≃ ye2) ∧ ye1 ≥ ye2"
          using DivNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_binary SignedFloatingIntegerDivNode)
        then have "∃ xe2 ye2. (g2 ⊢ n ≃ BinaryExpr BinDiv xe2 ye2) ∧ 
            BinaryExpr BinDiv xe1 ye1 ≥ BinaryExpr BinDiv xe2 ye2"
          by (metis DivNode.prems l mono_binary rep.DivNode xer)
        then show ?thesis
          by meson
      qed
    next
      case (ModNode n x y xe1 ye1)
      have k: "g1 ⊢ n ≃ BinaryExpr BinMod xe1 ye1" 
        using ModNode by (simp add: ModNode.hyps(2) rep.ModNode f)
      obtain xn yn where l: "kind g1 n = SignedFloatingIntegerRemNode xn yn"
        by (simp add: ModNode.hyps(1))
      then have mx: "g1 ⊢ xn ≃ xe1"
        using ModNode.hyps(1,2) by simp
      from l have my: "g1 ⊢ yn ≃ ye1"
        using ModNode.hyps(1,3) by simp
      then show ?case
      proof -
        have "g1 ⊢ xn ≃ xe1" 
          by (simp add: mx)
        have "g1 ⊢ yn ≃ ye1" 
          by (simp add: my)
        have xer: "∃ xe2. (g2 ⊢ xn ≃ xe2) ∧ xe1 ≥ xe2"
          using ModNode  a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_binary SignedFloatingIntegerRemNode)
        have "∃ ye2. (g2 ⊢ yn ≃ ye2) ∧ ye1 ≥ ye2"
          using ModNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_binary SignedFloatingIntegerRemNode)
        then have "∃ xe2 ye2. (g2 ⊢ n ≃ BinaryExpr BinMod xe2 ye2) ∧ 
            BinaryExpr BinMod xe1 ye1 ≥ BinaryExpr BinMod xe2 ye2"
          by (metis ModNode.prems l mono_binary rep.ModNode xer)
        then show ?thesis
          by meson
      qed
    next
      case (SubNode n x y xe1 ye1)
      have k: "g1 ⊢ n ≃ BinaryExpr BinSub xe1 ye1" 
        using SubNode by (simp add: SubNode.hyps(2) rep.SubNode f)
      obtain xn yn where l: "kind g1 n = SubNode xn yn"
        by (simp add: SubNode.hyps(1))
      then have mx: "g1 ⊢ xn ≃ xe1"
        using SubNode.hyps(1,2) by simp
      from l have my: "g1 ⊢ yn ≃ ye1"
        using SubNode.hyps(1,3) by simp
      then show ?case
      proof -
        have "g1 ⊢ xn ≃ xe1" 
          by (simp add: mx)
        have "g1 ⊢ yn ≃ ye1" 
          by (simp add: my)
        have xer: "∃ xe2. (g2 ⊢ xn ≃ xe2) ∧ xe1 ≥ xe2"
          using SubNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_binary SubNode)
        have "∃ ye2. (g2 ⊢ yn ≃ ye2) ∧ ye1 ≥ ye2"
          using SubNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_binary SubNode)
        then have "∃ xe2 ye2. (g2 ⊢ n ≃ BinaryExpr BinSub xe2 ye2) ∧ 
            BinaryExpr BinSub xe1 ye1 ≥ BinaryExpr BinSub xe2 ye2"
          by (metis SubNode.prems l mono_binary rep.SubNode xer)
        then show ?thesis
          by meson
      qed
    next
      case (AndNode n x y xe1 ye1)
      have k: "g1 ⊢ n ≃ BinaryExpr BinAnd xe1 ye1" 
        using AndNode by (simp add: AndNode.hyps(2) rep.AndNode f)
      obtain xn yn where l: "kind g1 n = AndNode xn yn"
        using AndNode.hyps(1) by simp
      then have mx: "g1 ⊢ xn ≃ xe1"
        using AndNode.hyps(1,2) by simp
      from l have my: "g1 ⊢ yn ≃ ye1"
        using AndNode.hyps(1,3) by simp
      then show ?case
      proof -
        have "g1 ⊢ xn ≃ xe1" 
          by (simp add: mx)
        have "g1 ⊢ yn ≃ ye1" 
          by (simp add: my)
        have xer: "∃ xe2. (g2 ⊢ xn ≃ xe2) ∧ xe1 ≥ xe2"
          using AndNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_binary AndNode)
        have "∃ ye2. (g2 ⊢ yn ≃ ye2) ∧ ye1 ≥ ye2"
          using AndNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_binary AndNode)
        then have "∃ xe2 ye2. (g2 ⊢ n ≃ BinaryExpr BinAnd xe2 ye2) ∧ 
            BinaryExpr BinAnd xe1 ye1 ≥ BinaryExpr BinAnd xe2 ye2"
          by (metis AndNode.prems l mono_binary rep.AndNode xer)
        then show ?thesis
          by meson
      qed
    next
      case (OrNode n x y xe1 ye1)
      have k: "g1 ⊢ n ≃ BinaryExpr BinOr xe1 ye1" 
        using OrNode by (simp add: OrNode.hyps(2) rep.OrNode f)
      obtain xn yn where l: "kind g1 n = OrNode xn yn"
        using OrNode.hyps(1) by simp
      then have mx: "g1 ⊢ xn ≃ xe1"
        using OrNode.hyps(1,2) by simp
      from l have my: "g1 ⊢ yn ≃ ye1"
        using OrNode.hyps(1,3) by simp
      then show ?case
      proof -
        have "g1 ⊢ xn ≃ xe1" 
          by (simp add: mx)
        have "g1 ⊢ yn ≃ ye1" 
          by (simp add: my)
        have xer: "∃ xe2. (g2 ⊢ xn ≃ xe2) ∧ xe1 ≥ xe2"
          using OrNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_binary OrNode)
        have "∃ ye2. (g2 ⊢ yn ≃ ye2) ∧ ye1 ≥ ye2"
          using OrNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_binary OrNode)
        then have "∃ xe2 ye2. (g2 ⊢ n ≃ BinaryExpr BinOr xe2 ye2) ∧ 
             BinaryExpr BinOr xe1 ye1 ≥ BinaryExpr BinOr xe2 ye2"
          by (metis OrNode.prems l mono_binary rep.OrNode xer)
        then show ?thesis
          by meson
      qed
    next
      case (XorNode n x y xe1 ye1)
      have k: "g1 ⊢ n ≃ BinaryExpr BinXor xe1 ye1" 
        using XorNode by (simp add: XorNode.hyps(2) rep.XorNode f)
      obtain xn yn where l: "kind g1 n = XorNode xn yn"
        using XorNode.hyps(1) by simp
      then have mx: "g1 ⊢ xn ≃ xe1"
        using XorNode.hyps(1,2) by simp
      from l have my: "g1 ⊢ yn ≃ ye1"
        using XorNode.hyps(1,3) by simp
      then show ?case
      proof -
        have "g1 ⊢ xn ≃ xe1" 
          by (simp add: mx)
        have "g1 ⊢ yn ≃ ye1" 
          by (simp add: my)
        have xer: "∃ xe2. (g2 ⊢ xn ≃ xe2) ∧ xe1 ≥ xe2"
          using XorNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_binary XorNode)
        have "∃ ye2. (g2 ⊢ yn ≃ ye2) ∧ ye1 ≥ ye2"
          using XorNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_binary XorNode)
        then have "∃ xe2 ye2. (g2 ⊢ n ≃ BinaryExpr BinXor xe2 ye2) ∧ 
            BinaryExpr BinXor xe1 ye1 ≥ BinaryExpr BinXor xe2 ye2"
          by (metis XorNode.prems l mono_binary rep.XorNode xer)
        then show ?thesis
          by meson
      qed
    next
    case (ShortCircuitOrNode n x y xe1 ye1)
    have k: "g1 ⊢ n ≃ BinaryExpr BinShortCircuitOr xe1 ye1" 
      using ShortCircuitOrNode by (simp add: ShortCircuitOrNode.hyps(2) rep.ShortCircuitOrNode f)
      obtain xn yn where l: "kind g1 n = ShortCircuitOrNode xn yn"
        using ShortCircuitOrNode.hyps(1) by simp
      then have mx: "g1 ⊢ xn ≃ xe1"
        using ShortCircuitOrNode.hyps(1,2) by simp
      from l have my: "g1 ⊢ yn ≃ ye1"
        using ShortCircuitOrNode.hyps(1,3) by simp
      then show ?case
      proof -
        have "g1 ⊢ xn ≃ xe1" 
          by (simp add: mx)
        have "g1 ⊢ yn ≃ ye1" 
          by (simp add: my)
        have xer: "∃ xe2. (g2 ⊢ xn ≃ xe2) ∧ xe1 ≥ xe2"
          using ShortCircuitOrNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_binary ShortCircuitOrNode)
        have "∃ ye2. (g2 ⊢ yn ≃ ye2) ∧ ye1 ≥ ye2"
          using ShortCircuitOrNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_binary ShortCircuitOrNode)
        then have "∃ xe2 ye2. (g2 ⊢ n ≃ BinaryExpr BinShortCircuitOr xe2 ye2) ∧ 
 BinaryExpr BinShortCircuitOr xe1 ye1 ≥ BinaryExpr BinShortCircuitOr xe2 ye2"
          by (metis ShortCircuitOrNode.prems l mono_binary rep.ShortCircuitOrNode xer)
        then show ?thesis
          by meson
      qed
    next
      case (LeftShiftNode n x y xe1 ye1)
      have k: "g1 ⊢ n ≃ BinaryExpr BinLeftShift xe1 ye1" 
        using LeftShiftNode by (simp add: LeftShiftNode.hyps(2) rep.LeftShiftNode f)
      obtain xn yn where l: "kind g1 n = LeftShiftNode xn yn"
        using LeftShiftNode.hyps(1) by simp
      then have mx: "g1 ⊢ xn ≃ xe1"
        using LeftShiftNode.hyps(1,2) by simp
      from l have my: "g1 ⊢ yn ≃ ye1"
        using LeftShiftNode.hyps(1,3) by simp
      then show ?case
      proof -
        have "g1 ⊢ xn ≃ xe1" 
          by (simp add: mx)
        have "g1 ⊢ yn ≃ ye1" 
          by (simp add: my)
        have xer: "∃ xe2. (g2 ⊢ xn ≃ xe2) ∧ xe1 ≥ xe2"
          using LeftShiftNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_binary LeftShiftNode)
        have "∃ ye2. (g2 ⊢ yn ≃ ye2) ∧ ye1 ≥ ye2"
          using LeftShiftNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_binary LeftShiftNode)
        then have "∃ xe2 ye2. (g2 ⊢ n ≃ BinaryExpr BinLeftShift xe2 ye2) ∧ 
      BinaryExpr BinLeftShift xe1 ye1 ≥ BinaryExpr BinLeftShift xe2 ye2"
          by (metis LeftShiftNode.prems l mono_binary rep.LeftShiftNode xer)
        then show ?thesis
          by meson
      qed
    next
      case (RightShiftNode n x y xe1 ye1)
      have k: "g1 ⊢ n ≃ BinaryExpr BinRightShift xe1 ye1" 
        using RightShiftNode by (simp add: RightShiftNode.hyps(2) rep.RightShiftNode)
      obtain xn yn where l: "kind g1 n = RightShiftNode xn yn"
        using RightShiftNode.hyps(1) by simp
      then have mx: "g1 ⊢ xn ≃ xe1"
        using RightShiftNode.hyps(1,2) by simp
      from l have my: "g1 ⊢ yn ≃ ye1"
        using RightShiftNode.hyps(1,3) by simp
      then show ?case
      proof -
        have "g1 ⊢ xn ≃ xe1" 
          by (simp add: mx)
        have "g1 ⊢ yn ≃ ye1" 
          by (simp add: my)
        have xer: "∃ xe2. (g2 ⊢ xn ≃ xe2) ∧ xe1 ≥ xe2"
          using RightShiftNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_binary RightShiftNode)
        have "∃ ye2. (g2 ⊢ yn ≃ ye2) ∧ ye1 ≥ ye2"
          using RightShiftNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_binary RightShiftNode)
        then have "∃ xe2 ye2. (g2 ⊢ n ≃ BinaryExpr BinRightShift xe2 ye2) ∧ 
     BinaryExpr BinRightShift xe1 ye1 ≥ BinaryExpr BinRightShift xe2 ye2"
          by (metis RightShiftNode.prems l mono_binary rep.RightShiftNode xer)
        then show ?thesis
          by meson
      qed
    next
      case (UnsignedRightShiftNode n x y xe1 ye1)
      have k: "g1 ⊢ n ≃ BinaryExpr BinURightShift xe1 ye1" 
        using UnsignedRightShiftNode by (simp add: UnsignedRightShiftNode.hyps(2) 
                                                   rep.UnsignedRightShiftNode)
      obtain xn yn where l: "kind g1 n = UnsignedRightShiftNode xn yn"
        using UnsignedRightShiftNode.hyps(1) by simp
      then have mx: "g1 ⊢ xn ≃ xe1"
        using UnsignedRightShiftNode.hyps(1,2) by simp
      from l have my: "g1 ⊢ yn ≃ ye1"
        using UnsignedRightShiftNode.hyps(1,3) by simp
      then show ?case
      proof -
        have "g1 ⊢ xn ≃ xe1" 
          by (simp add: mx)
        have "g1 ⊢ yn ≃ ye1" 
          by (simp add: my)
        have xer: "∃ xe2. (g2 ⊢ xn ≃ xe2) ∧ xe1 ≥ xe2"
          using UnsignedRightShiftNode a b c d no_encoding not_excluded_keep_type repDet singletonD 
                l
          by (metis_node_eq_binary UnsignedRightShiftNode)
        have "∃ ye2. (g2 ⊢ yn ≃ ye2) ∧ ye1 ≥ ye2"
          using UnsignedRightShiftNode a b c d no_encoding not_excluded_keep_type repDet singletonD 
                l
          by (metis_node_eq_binary UnsignedRightShiftNode)
        then have "∃ xe2 ye2. (g2 ⊢ n ≃ BinaryExpr BinURightShift xe2 ye2) ∧ 
    BinaryExpr BinURightShift xe1 ye1 ≥ BinaryExpr BinURightShift xe2 ye2"
          by (metis UnsignedRightShiftNode.prems l mono_binary rep.UnsignedRightShiftNode xer)
        then show ?thesis
          by meson
      qed
    next
      case (IntegerBelowNode n x y xe1 ye1)
      have k: "g1 ⊢ n ≃ BinaryExpr BinIntegerBelow xe1 ye1" 
        using IntegerBelowNode by (simp add: IntegerBelowNode.hyps(2) rep.IntegerBelowNode)
      obtain xn yn where l: "kind g1 n = IntegerBelowNode xn yn"
        using IntegerBelowNode.hyps(1) by simp
      then have mx: "g1 ⊢ xn ≃ xe1"
        using IntegerBelowNode.hyps(1,2) by simp
      from l have my: "g1 ⊢ yn ≃ ye1"
        using IntegerBelowNode.hyps(1,3) by simp
      then show ?case
      proof -
        have "g1 ⊢ xn ≃ xe1" 
          by (simp add: mx)
        have "g1 ⊢ yn ≃ ye1" 
          by (simp add: my)
        have xer: "∃ xe2. (g2 ⊢ xn ≃ xe2) ∧ xe1 ≥ xe2"
          using IntegerBelowNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_binary IntegerBelowNode)
        have "∃ ye2. (g2 ⊢ yn ≃ ye2) ∧ ye1 ≥ ye2"
          using IntegerBelowNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_binary IntegerBelowNode)
        then have "∃ xe2 ye2. (g2 ⊢ n ≃ BinaryExpr BinIntegerBelow xe2 ye2) ∧ 
   BinaryExpr BinIntegerBelow xe1 ye1 ≥ BinaryExpr BinIntegerBelow xe2 ye2"
          by (metis IntegerBelowNode.prems l mono_binary rep.IntegerBelowNode xer)
        then show ?thesis
          by meson
      qed
    next
      case (IntegerEqualsNode n x y xe1 ye1)
      have k: "g1 ⊢ n ≃ BinaryExpr BinIntegerEquals xe1 ye1" 
        using IntegerEqualsNode by (simp add: IntegerEqualsNode.hyps(2) rep.IntegerEqualsNode)
      obtain xn yn where l: "kind g1 n = IntegerEqualsNode xn yn"
        using IntegerEqualsNode.hyps(1) by simp
      then have mx: "g1 ⊢ xn ≃ xe1"
        using IntegerEqualsNode.hyps(1,2) by simp
      from l have my: "g1 ⊢ yn ≃ ye1"
        using IntegerEqualsNode.hyps(1,3) by simp
      then show ?case
      proof -
        have "g1 ⊢ xn ≃ xe1" 
          by (simp add: mx)
        have "g1 ⊢ yn ≃ ye1" 
          by (simp add: my)
        have xer: "∃ xe2. (g2 ⊢ xn ≃ xe2) ∧ xe1 ≥ xe2"
          using IntegerEqualsNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_binary IntegerEqualsNode)
        have "∃ ye2. (g2 ⊢ yn ≃ ye2) ∧ ye1 ≥ ye2"
          using IntegerEqualsNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_binary IntegerEqualsNode)
        then have "∃ xe2 ye2. (g2 ⊢ n ≃ BinaryExpr BinIntegerEquals xe2 ye2) ∧ 
  BinaryExpr BinIntegerEquals xe1 ye1 ≥ BinaryExpr BinIntegerEquals xe2 ye2"
          by (metis IntegerEqualsNode.prems l mono_binary rep.IntegerEqualsNode xer)
        then show ?thesis
          by meson
      qed
    next
      case (IntegerLessThanNode n x y xe1 ye1)
      have k: "g1 ⊢ n ≃ BinaryExpr BinIntegerLessThan xe1 ye1" 
        using IntegerLessThanNode by (simp add: IntegerLessThanNode.hyps(2) rep.IntegerLessThanNode)
      obtain xn yn where l: "kind g1 n = IntegerLessThanNode xn yn"
        using IntegerLessThanNode.hyps(1) by simp
      then have mx: "g1 ⊢ xn ≃ xe1"
        using IntegerLessThanNode.hyps(1,2) by simp
      from l have my: "g1 ⊢ yn ≃ ye1"
        using IntegerLessThanNode.hyps(1,3) by simp
      then show ?case
      proof -
        have "g1 ⊢ xn ≃ xe1" 
          by (simp add: mx)
        have "g1 ⊢ yn ≃ ye1" 
          by (simp add: my)
        have xer: "∃ xe2. (g2 ⊢ xn ≃ xe2) ∧ xe1 ≥ xe2"
          using IntegerLessThanNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_binary IntegerLessThanNode)
        have "∃ ye2. (g2 ⊢ yn ≃ ye2) ∧ ye1 ≥ ye2"
          using IntegerLessThanNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis_node_eq_binary IntegerLessThanNode)
        then have "∃ xe2 ye2. (g2 ⊢ n ≃ BinaryExpr BinIntegerLessThan xe2 ye2) ∧ 
BinaryExpr BinIntegerLessThan xe1 ye1 ≥ BinaryExpr BinIntegerLessThan xe2 ye2"
          by (metis IntegerLessThanNode.prems l mono_binary rep.IntegerLessThanNode xer)
        then show ?thesis
          by meson
      qed
    next
      case (IntegerTestNode n x y xe1 ye1)
      have k: "g1 ⊢ n ≃ BinaryExpr BinIntegerTest xe1 ye1" 
        using IntegerTestNode by (meson rep.IntegerTestNode) 
      obtain xn yn where l: "kind g1 n = IntegerTestNode xn yn"
        by (simp add: IntegerTestNode.hyps(1))
      then have mx: "g1 ⊢ xn ≃ xe1"
        using IRNode.inject(21) IntegerTestNode.hyps(1,2) by presburger
      from l have my: "g1 ⊢ yn ≃ ye1"
        by (metis IRNode.inject(21) IntegerTestNode.hyps(1,3))
      then show ?case
      proof -
        have "g1 ⊢ xn ≃ xe1"
          by (simp add: mx)
        have "g1 ⊢ yn ≃ ye1"
          by (simp add: my)
        have xer: "∃ xe2. (g2 ⊢ xn ≃ xe2) ∧ xe1 ≥ xe2"
          using IntegerTestNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis IRNode.inject(21))
        have "∃ ye2. (g2 ⊢ yn ≃ ye2) ∧ ye1 ≥ ye2"
          using IntegerLessThanNode a b c d l no_encoding not_excluded_keep_type repDet singletonD
          by (metis IRNode.inject(21) IntegerTestNode.IH(2) IntegerTestNode.hyps(1) my)
        then have "∃ xe2 ye2. (g2 ⊢ n ≃ BinaryExpr BinIntegerTest xe2 ye2) ∧ 
    BinaryExpr BinIntegerTest xe1 ye1 ≥ BinaryExpr BinIntegerTest xe2 ye2"
          by (metis IntegerTestNode.prems l mono_binary xer rep.IntegerTestNode)
        then show ?thesis
          by meson
      qed
    next
      case (IntegerNormalizeCompareNode n x y xe1 ye1)
      have k: "g1 ⊢ n ≃ BinaryExpr BinIntegerNormalizeCompare xe1 ye1"
        by (simp add: IntegerNormalizeCompareNode.hyps(1,2,3) rep.IntegerNormalizeCompareNode)
      obtain xn yn where l: "kind g1 n = IntegerNormalizeCompareNode xn yn"
        by (simp add: IntegerNormalizeCompareNode.hyps(1))
      then have mx: "g1 ⊢ xn ≃ xe1"
        using IRNode.inject(20) IntegerNormalizeCompareNode.hyps(1,2) by presburger
      from l have my: "g1 ⊢ yn ≃ ye1"
        using IRNode.inject(20) IntegerNormalizeCompareNode.hyps(1,3) by presburger
      then show ?case
      proof -
        have "g1 ⊢ xn ≃ xe1"
          by (simp add: mx)
        have "g1 ⊢ yn ≃ ye1"
          by (simp add: my)
        have xer: "∃ xe2. (g2 ⊢ xn ≃ xe2) ∧ xe1 ≥ xe2"
          by (metis IRNode.inject(20) IntegerNormalizeCompareNode.IH(1) l mx no_encoding a b c d
              IntegerNormalizeCompareNode.hyps(1) emptyE insertE not_excluded_keep_type repDet)
        have "∃ ye2. (g2 ⊢ yn ≃ ye2) ∧ ye1 ≥ ye2"
          by (metis IRNode.inject(20) IntegerNormalizeCompareNode.IH(2) my no_encoding a b c d l
              IntegerNormalizeCompareNode.hyps(1) emptyE insertE not_excluded_keep_type repDet)
        then have "∃ xe2 ye2. (g2 ⊢ n ≃ BinaryExpr BinIntegerNormalizeCompare xe2 ye2) ∧
    BinaryExpr BinIntegerNormalizeCompare xe1 ye1 ≥ BinaryExpr BinIntegerNormalizeCompare xe2 ye2"
          by (metis IntegerNormalizeCompareNode.prems l mono_binary rep.IntegerNormalizeCompareNode
              xer)
        then show ?thesis
          by meson
      qed
    next
      case (IntegerMulHighNode n x y xe1 ye1)
      have k: "g1 ⊢ n ≃ BinaryExpr BinIntegerMulHigh xe1 ye1"
        by (simp add: IntegerMulHighNode.hyps(1,2,3) rep.IntegerMulHighNode)
      obtain xn yn where l: "kind g1 n = IntegerMulHighNode xn yn"
        by (simp add: IntegerMulHighNode.hyps(1))
      then have mx: "g1 ⊢ xn ≃ xe1"
        using IRNode.inject(19) IntegerMulHighNode.hyps(1,2) by presburger
      from l have my: "g1 ⊢ yn ≃ ye1"
        using IRNode.inject(19) IntegerMulHighNode.hyps(1,3) by presburger
      then show ?case
      proof -
        have "g1 ⊢ xn ≃ xe1"
          by (simp add: mx)
        have "g1 ⊢ yn ≃ ye1"
          by (simp add: my)
        have xer: "∃ xe2. (g2 ⊢ xn ≃ xe2) ∧ xe1 ≥ xe2"
          by (metis IRNode.inject(19) IntegerMulHighNode.IH(1) IntegerMulHighNode.hyps(1) a b c d
              emptyE insertE l mx no_encoding not_excluded_keep_type repDet)
        have "∃ ye2. (g2 ⊢ yn ≃ ye2) ∧ ye1 ≥ ye2"
          by (metis IRNode.inject(19) IntegerMulHighNode.IH(2) IntegerMulHighNode.hyps(1) a b c d
              emptyE insertE l my no_encoding not_excluded_keep_type repDet)
        then have "∃ xe2 ye2. (g2 ⊢ n ≃ BinaryExpr BinIntegerMulHigh xe2 ye2) ∧
 BinaryExpr BinIntegerMulHigh xe1 ye1 ≥ BinaryExpr BinIntegerMulHigh xe2 ye2"
          by (metis IntegerMulHighNode.prems l mono_binary rep.IntegerMulHighNode xer)
        then show ?thesis
          by meson
      qed
    next
      case (NarrowNode n inputBits resultBits x xe1)
      have k: "g1 ⊢ n ≃ UnaryExpr (UnaryNarrow inputBits resultBits) xe1" 
        using NarrowNode by (simp add: NarrowNode.hyps(2) rep.NarrowNode)
      obtain xn where l: "kind g1 n = NarrowNode inputBits resultBits xn"
        using NarrowNode.hyps(1) by simp
      then have m: "g1 ⊢ xn ≃ xe1"
        using NarrowNode.hyps(1,2) by simp
      then show ?case
      proof (cases "xn = n'")
        case True
        then have n: "xe1 = e1'" 
          using m by (simp add: repDet c)
        then have ev: "g2 ⊢ n ≃ UnaryExpr (UnaryNarrow inputBits resultBits) e2'" 
          using l by (simp add: rep.NarrowNode d True NarrowNode.prems)
        then have r: "UnaryExpr (UnaryNarrow inputBits resultBits) e1' ≥ 
                      UnaryExpr (UnaryNarrow inputBits resultBits) e2'"
          by (meson a mono_unary)
        then show ?thesis
          by (metis n ev)
      next
        case False
        have "g1 ⊢ xn ≃ xe1" 
          by (simp add: m)
        have "∃ xe2. (g2 ⊢ xn ≃ xe2) ∧ xe1 ≥ xe2"
          using NarrowNode False b encodes_contains l not_excluded_keep_type not_in_g singleton_iff
          by (metis_node_eq_ternary NarrowNode)
        then have "∃ xe2. (g2 ⊢ n ≃ UnaryExpr (UnaryNarrow inputBits resultBits) xe2) ∧ 
                                    UnaryExpr (UnaryNarrow inputBits resultBits) xe1 ≥ 
                                    UnaryExpr (UnaryNarrow inputBits resultBits) xe2"
          by (metis NarrowNode.prems l mono_unary rep.NarrowNode)
        then show ?thesis
          by meson
      qed
    next
      case (SignExtendNode n inputBits resultBits x xe1)
      have k: "g1 ⊢ n ≃ UnaryExpr (UnarySignExtend inputBits resultBits) xe1" 
        using SignExtendNode by (simp add: SignExtendNode.hyps(2) rep.SignExtendNode)
      obtain xn where l: "kind g1 n = SignExtendNode inputBits resultBits xn"
        using SignExtendNode.hyps(1) by simp
      then have m: "g1 ⊢ xn ≃ xe1"
        using SignExtendNode.hyps(1,2) by simp
      then show ?case
      proof (cases "xn = n'")
        case True
        then have n: "xe1 = e1'" 
          using m by (simp add: repDet c)
        then have ev: "g2 ⊢ n ≃ UnaryExpr (UnarySignExtend inputBits resultBits) e2'" 
          using l by (simp add: True d rep.SignExtendNode SignExtendNode.prems)
        then have r: "UnaryExpr (UnarySignExtend inputBits resultBits) e1' ≥ 
                      UnaryExpr (UnarySignExtend inputBits resultBits) e2'"
          by (meson a mono_unary)
        then show ?thesis
          by (metis n ev)
      next
        case False
        have "g1 ⊢ xn ≃ xe1" 
          by (simp add: m)
        have "∃ xe2. (g2 ⊢ xn ≃ xe2) ∧ xe1 ≥ xe2"
          using SignExtendNode False b encodes_contains l not_excluded_keep_type not_in_g 
                singleton_iff
          by (metis_node_eq_ternary SignExtendNode)
        then have "∃ xe2. (g2 ⊢ n ≃ UnaryExpr (UnarySignExtend inputBits resultBits) xe2) ∧ 
                                    UnaryExpr (UnarySignExtend inputBits resultBits) xe1 ≥ 
                                    UnaryExpr (UnarySignExtend inputBits resultBits) xe2"
          by (metis SignExtendNode.prems l mono_unary rep.SignExtendNode)
        then show ?thesis
          by meson
      qed
    next
      case (ZeroExtendNode n inputBits resultBits x xe1)
      have k: "g1 ⊢ n ≃ UnaryExpr (UnaryZeroExtend inputBits resultBits) xe1" 
        using ZeroExtendNode by (simp add: ZeroExtendNode.hyps(2) rep.ZeroExtendNode)
      obtain xn where l: "kind g1 n = ZeroExtendNode inputBits resultBits xn"
        using ZeroExtendNode.hyps(1) by simp
      then have m: "g1 ⊢ xn ≃ xe1"
        using ZeroExtendNode.hyps(1,2) by simp
      then show ?case
      proof (cases "xn = n'")
        case True
        then have n: "xe1 = e1'" 
          using m by (simp add: repDet c)
        then have ev: "g2 ⊢ n ≃ UnaryExpr (UnaryZeroExtend inputBits resultBits) e2'" 
          using l by (simp add: ZeroExtendNode.prems True d rep.ZeroExtendNode)
        then have r: "UnaryExpr (UnaryZeroExtend inputBits resultBits) e1' ≥ 
                      UnaryExpr (UnaryZeroExtend inputBits resultBits) e2'"
          by (meson a mono_unary)
        then show ?thesis
          by (metis n ev)
      next
        case False
        have "g1 ⊢ xn ≃ xe1" 
          by (simp add: m)
        have "∃ xe2. (g2 ⊢ xn ≃ xe2) ∧ xe1 ≥ xe2"
          using ZeroExtendNode b encodes_contains l not_excluded_keep_type not_in_g singleton_iff 
                False
          by (metis_node_eq_ternary ZeroExtendNode)
        then have "∃ xe2. (g2 ⊢ n ≃ UnaryExpr (UnaryZeroExtend inputBits resultBits) xe2) ∧ 
                                    UnaryExpr (UnaryZeroExtend inputBits resultBits) xe1 ≥ 
                                    UnaryExpr (UnaryZeroExtend inputBits resultBits) xe2"
          by (metis ZeroExtendNode.prems l mono_unary rep.ZeroExtendNode)
        then show ?thesis
          by meson
      qed
    next
      case (LeafNode n s)
      then show ?case
        by (metis eq_refl rep.LeafNode)
    next
      case (PiNode n' gu)
      then show ?case
        by (metis encodes_contains not_excluded_keep_type not_in_g rep.PiNode repDet singleton_iff
            a b c d)
    next
      case (RefNode n')
      then show ?case
        by (metis a b c d no_encoding not_excluded_keep_type rep.RefNode repDet singletonD)
    next
      case (IsNullNode n)
      then show ?case
        by (metis insertE mono_unary no_encoding not_excluded_keep_type rep.IsNullNode repDet emptyE 
            a b c d) 
    qed
  qed
qed

lemma graph_semantics_preservation_subscript:
  assumes a: "e⇩1' ≥ e⇩2'"
  assumes b: "({n} ⊴ as_set g⇩1) ⊆ as_set g⇩2"
  assumes c: "g⇩1 ⊢ n ≃ e⇩1'"
  assumes d: "g⇩2 ⊢ n ≃ e⇩2'"
  shows "graph_refinement g⇩1 g⇩2"
  using assms by (simp add: graph_semantics_preservation)

lemma tree_to_graph_rewriting:
  "e⇩1 ≥ e⇩2 
  ∧ (g⇩1 ⊢ n ≃ e⇩1) ∧ maximal_sharing g⇩1
  ∧ ({n} ⊴ as_set g⇩1) ⊆ as_set g⇩2 
  ∧ (g⇩2 ⊢ n ≃ e⇩2) ∧ maximal_sharing g⇩2
  ⟹ graph_refinement g⇩1 g⇩2"
  by (auto simp add: graph_semantics_preservation)

declare [[simp_trace]]
lemma equal_refines:
  fixes e1 e2 :: IRExpr
  assumes "e1 = e2"
  shows "e1 ≥ e2"
  using assms by simp
declare [[simp_trace=false]]

inductive_cases UnaryRepE[elim!]:✐‹tag invisible›
  "g ⊢ n ≃ (UnaryExpr op xe)"
inductive_cases BinaryRepE[elim!]:✐‹tag invisible›
  "g ⊢ n ≃ (BinaryExpr op xe ye)"

lemma eval_contains_id[simp]: "g1 ⊢ n ≃ e ⟹ n ∈ ids g1"
  using no_encoding by auto

lemma subset_kind[simp]: "as_set g1 ⊆ as_set g2 ⟹ g1 ⊢ n ≃ e ⟹ kind g1 n = kind g2 n"
  using eval_contains_id as_set_def by blast

lemma subset_stamp[simp]: "as_set g1 ⊆ as_set g2 ⟹ g1 ⊢ n ≃ e ⟹ stamp g1 n = stamp g2 n"
  using eval_contains_id as_set_def by blast

method solve_subset_eval uses as_set eval =
  (metis eval as_set subset_kind subset_stamp |
   metis eval as_set subset_kind)

(*
lemmas rep_rules =
  ConstantNode
  ParameterNode
  ConditionalNode

method solve_subset_eval uses as_set =
  (match premises in "kind _ _ = node _ ⟹ _" for node ⇒
    ‹match rep_rules in eval: "kind _ _ = node _ ⟹ _" ⇒ 
       ‹metis eval as_set subset_kind››)

method solve_subset_debug uses as_set =
  (match premises in k: "kind _ _ = node _ _" for node ⇒
    ‹match rep_rules in eval: "kind _ _ = node _ _ ⟹ _" ⇒ 
       ‹print_term node››)
*)

lemma subset_implies_evals:
  assumes "as_set g1 ⊆ as_set g2"
  assumes "(g1 ⊢ n ≃ e)"
  shows "(g2 ⊢ n ≃ e)"
  using assms(2)
  apply (induction e)
                          apply (solve_subset_eval as_set: assms(1) eval: ConstantNode)
                         apply (solve_subset_eval as_set: assms(1) eval: ParameterNode)
                        apply (solve_subset_eval as_set: assms(1) eval: ConditionalNode)
                       apply (solve_subset_eval as_set: assms(1) eval: AbsNode)
                      apply (solve_subset_eval as_set: assms(1) eval: ReverseBytesNode)
                     apply (solve_subset_eval as_set: assms(1) eval: BitCountNode)
                      apply (solve_subset_eval as_set: assms(1) eval: NotNode)
                     apply (solve_subset_eval as_set: assms(1) eval: NegateNode)
                    apply (solve_subset_eval as_set: assms(1) eval: LogicNegationNode)
                   apply (solve_subset_eval as_set: assms(1) eval: AddNode)
                   apply (solve_subset_eval as_set: assms(1) eval: MulNode)
                   apply (solve_subset_eval as_set: assms(1) eval: DivNode)
                  apply (solve_subset_eval as_set: assms(1) eval: ModNode)
                 apply (solve_subset_eval as_set: assms(1) eval: SubNode)
                apply (solve_subset_eval as_set: assms(1) eval: AndNode)
               apply (solve_subset_eval as_set: assms(1) eval: OrNode)
              apply (solve_subset_eval as_set: assms(1) eval: XorNode)
             apply (solve_subset_eval as_set: assms(1) eval: ShortCircuitOrNode)
            apply (solve_subset_eval as_set: assms(1) eval: LeftShiftNode)
           apply (solve_subset_eval as_set: assms(1) eval: RightShiftNode)
          apply (solve_subset_eval as_set: assms(1) eval: UnsignedRightShiftNode)
         apply (solve_subset_eval as_set: assms(1) eval: IntegerBelowNode)
        apply (solve_subset_eval as_set: assms(1) eval: IntegerEqualsNode)
       apply (solve_subset_eval as_set: assms(1) eval: IntegerLessThanNode)
       apply (solve_subset_eval as_set: assms(1) eval: IntegerTestNode)
      apply (solve_subset_eval as_set: assms(1) eval: IntegerNormalizeCompareNode)
      apply (solve_subset_eval as_set: assms(1) eval: IntegerMulHighNode)
      apply (solve_subset_eval as_set: assms(1) eval: NarrowNode)
     apply (solve_subset_eval as_set: assms(1) eval: SignExtendNode)
    apply (solve_subset_eval as_set: assms(1) eval: ZeroExtendNode)
   apply (solve_subset_eval as_set: assms(1) eval: LeafNode)
      apply (solve_subset_eval as_set: assms(1) eval: PiNode)
  apply (solve_subset_eval as_set: assms(1) eval: RefNode)
  by (solve_subset_eval as_set: assms(1) eval: IsNullNode)

lemma subset_refines:
  assumes "as_set g1 ⊆ as_set g2"
  shows "graph_refinement g1 g2"
proof -
  have "ids g1 ⊆ ids g2" 
    using assms as_set_def by blast
  then show ?thesis 
    unfolding graph_refinement_def 
    apply rule apply (rule allI) apply (rule impI) apply (rule allI) apply (rule impI)
    unfolding graph_represents_expression_def
    proof -
      fix n e1
      assume 1:"n ∈ ids g1"
      assume 2:"g1 ⊢ n ≃ e1"
      show "∃e2. (g2 ⊢ n ≃ e2) ∧ e1 ≥ e2"
        by (meson equal_refines subset_implies_evals assms 1 2)
    qed
  qed

lemma graph_construction:
  "e⇩1 ≥ e⇩2
  ∧ as_set g⇩1 ⊆ as_set g⇩2
  ∧ (g⇩2 ⊢ n ≃ e⇩2)
  ⟹ (g⇩2 ⊢ n ⊴ e⇩1) ∧ graph_refinement g⇩1 g⇩2"
  by (meson encodeeval.simps graph_represents_expression_def le_expr_def subset_refines)

subsubsection ‹Term Graph Reconstruction›

lemma find_exists_kind:
  assumes "find_node_and_stamp g (node, s) = Some nid"
  shows "kind g nid = node"
  by (metis (mono_tags, lifting) find_Some_iff find_node_and_stamp.simps assms)

lemma find_exists_stamp:
  assumes "find_node_and_stamp g (node, s) = Some nid"
  shows "stamp g nid = s"
  by (metis (mono_tags, lifting) find_Some_iff find_node_and_stamp.simps assms)

lemma find_new_kind:
  assumes "g' = add_node nid (node, s) g"
  assumes "node ≠ NoNode"
  shows "kind g' nid = node"
  by (simp add: add_node_lookup assms)

lemma find_new_stamp:
  assumes "g' = add_node nid (node, s) g"
  assumes "node ≠ NoNode"
  shows "stamp g' nid = s"
  by (simp add: assms add_node_lookup)

lemma sorted_bottom:
  assumes "finite xs"
  assumes "x ∈ xs"
  shows "x ≤ last(sorted_list_of_set(xs::nat set))"
  proof -
  obtain largest where largest: "largest = last (sorted_list_of_set(xs))"
    by simp
  obtain sortedList where sortedList: "sortedList = sorted_list_of_set(xs)"
    by simp
  have step: "∀i. 0 < i ∧ i < (length (sortedList)) ⟶ sortedList!(i-1) ≤ sortedList!(i)"
    unfolding sortedList apply auto
    by (metis diff_le_self sorted_list_of_set.length_sorted_key_list_of_set sorted_nth_mono
        sorted_list_of_set(2))
  have finalElement: "last (sorted_list_of_set(xs)) =
                                       sorted_list_of_set(xs)!(length (sorted_list_of_set(xs)) - 1)"
    using assms last_conv_nth sorted_list_of_set.sorted_key_list_of_set_eq_Nil_iff by blast
  have contains0: "(x ∈ xs) = (x ∈ set (sorted_list_of_set(xs)))"
    using assms(1) by auto
  have lastLargest: "((x ∈ xs) ⟶ (largest ≥ x))"
    using step unfolding largest finalElement apply auto
    by (metis (no_types, lifting) One_nat_def Suc_pred assms(1) card_Diff1_less in_set_conv_nth
        sorted_list_of_set.length_sorted_key_list_of_set card_Diff_singleton_if less_Suc_eq_le
        sorted_list_of_set.sorted_sorted_key_list_of_set length_pos_if_in_set sorted_nth_mono
        contains0)
  then show ?thesis
    by (simp add: assms largest)
qed

lemma fresh: "finite xs ⟹ last(sorted_list_of_set(xs::nat set)) + 1 ∉ xs"
  using sorted_bottom not_le by auto

lemma fresh_ids:
  assumes "n = get_fresh_id g"
  shows "n ∉ ids g"
proof -
  have "finite (ids g)" 
    by (simp add: Rep_IRGraph)
  then show ?thesis
    using assms fresh unfolding get_fresh_id.simps by blast
qed

lemma graph_unchanged_rep_unchanged:
  assumes "∀n ∈ ids g. kind g n = kind g' n"
  assumes "∀n ∈ ids g. stamp g n = stamp g' n"
  shows "(g ⊢ n ≃ e) ⟶ (g' ⊢ n ≃ e)"
  apply (rule impI) subgoal premises e using e assms
    apply (induction n e)
                          apply (metis no_encoding rep.ConstantNode)
                         apply (metis no_encoding rep.ParameterNode)
                        apply (metis no_encoding rep.ConditionalNode)
                       apply (metis no_encoding rep.AbsNode)
                      apply (metis no_encoding rep.ReverseBytesNode)
                      apply (metis no_encoding rep.BitCountNode)
                      apply (metis no_encoding rep.NotNode)
                     apply (metis no_encoding rep.NegateNode)
                    apply (metis no_encoding rep.LogicNegationNode)
                   apply (metis no_encoding rep.AddNode)
                   apply (metis no_encoding rep.MulNode)
                   apply (metis no_encoding rep.DivNode)
                  apply (metis no_encoding rep.ModNode)
                 apply (metis no_encoding rep.SubNode)
                apply (metis no_encoding rep.AndNode)
               apply (metis no_encoding rep.OrNode)
                apply (metis no_encoding rep.XorNode)
               apply (metis no_encoding rep.ShortCircuitOrNode)
              apply (metis no_encoding rep.LeftShiftNode)
             apply (metis no_encoding rep.RightShiftNode)
            apply (metis no_encoding rep.UnsignedRightShiftNode)
           apply (metis no_encoding rep.IntegerBelowNode)
          apply (metis no_encoding rep.IntegerEqualsNode)
         apply (metis no_encoding rep.IntegerLessThanNode)
         apply (metis no_encoding rep.IntegerTestNode)
        apply (metis no_encoding rep.IntegerNormalizeCompareNode)
        apply (metis no_encoding rep.IntegerMulHighNode)
        apply (metis no_encoding rep.NarrowNode)
       apply (metis no_encoding rep.SignExtendNode)
      apply (metis no_encoding rep.ZeroExtendNode)
     apply (metis no_encoding rep.LeafNode)
      apply (metis no_encoding rep.PiNode)
    apply (metis no_encoding rep.RefNode)
   by (metis no_encoding rep.IsNullNode)
  done

lemma fresh_node_subset:
  assumes "n ∉ ids g"
  assumes "g' = add_node n (k, s) g"
  shows "as_set g ⊆ as_set g'"
  by (smt (z3) Collect_mono_iff Diff_idemp Diff_insert_absorb add_changed as_set_def unchanged.simps
      disjoint_change assms)

lemma unique_subset:
  assumes "unique g node (g', n)"
  shows "as_set g ⊆ as_set g'"
  using assms fresh_ids fresh_node_subset
  by (metis Pair_inject old.prod.exhaust subsetI unique.cases)

lemma unrep_subset:
  assumes "(g ⊕ e ↝ (g', n))"
  shows "as_set g ⊆ as_set g'"
  using assms 
proof (induction g e "(g', n)" arbitrary: g' n)
  case (UnrepConstantNode g c n g')
  then show ?case using unique_subset by simp
next
  case (UnrepParameterNode g i s n)
  then show ?case using unique_subset by simp
next
  case (UnrepConditionalNode g ce g2 c te g3 t fe g4 f s' n)
  then show ?case using unique_subset by blast
next
  case (UnrepUnaryNode g xe g2 x s' op n)
  then show ?case using unique_subset by blast
next
  case (UnrepBinaryNode g xe g2 x ye g3 y s' op n)
  then show ?case using unique_subset by blast
next
  case (AllLeafNodes g n s)
  then show ?case 
    by auto
qed

lemma fresh_node_preserves_other_nodes:
  assumes "n' = get_fresh_id g"
  assumes "g' = add_node n' (k, s) g"
  shows "∀ n ∈ ids g . (g ⊢ n ≃ e) ⟶ (g' ⊢ n ≃ e)"
  using assms apply auto
  by (metis fresh_node_subset subset_implies_evals fresh_ids assms)

lemma found_node_preserves_other_nodes:
  assumes "find_node_and_stamp g (k, s) = Some n"
  shows "∀ n ∈ ids g. (g ⊢ n ≃ e) ⟷ (g ⊢ n ≃ e)"
  by (auto simp add: assms) 

lemma unrep_ids_subset[simp]:
  assumes "g ⊕ e ↝ (g', n)"
  shows "ids g ⊆ ids g'"
  by (meson graph_refinement_def subset_refines unrep_subset assms)

lemma unrep_unchanged:
  assumes "g ⊕ e ↝ (g', n)"
  shows "∀ n ∈ ids g . ∀ e. (g ⊢ n ≃ e) ⟶ (g' ⊢ n ≃ e)"
  by (meson subset_implies_evals unrep_subset assms)

lemma unique_kind:
  assumes "unique g (node, s) (g', nid)"
  assumes "node ≠ NoNode"
  shows "kind g' nid = node ∧ stamp g' nid = s"
  using assms find_exists_kind add_node_lookup
  by (smt (verit, del_insts) Pair_inject find_exists_stamp unique.cases)

lemma unique_eval:
  assumes "unique g (n, s) (g', nid)"
  shows "g ⊢ nid' ≃ e ⟹ g' ⊢ nid' ≃ e"
  using assms subset_implies_evals unique_subset by blast

lemma unrep_eval:
  assumes "unrep g e (g', nid)"
  shows "g ⊢ nid' ≃ e' ⟹ g' ⊢ nid' ≃ e'"
  using assms subset_implies_evals no_encoding unrep_unchanged by blast


lemma unary_node_nonode:
  "unary_node op x ≠ NoNode"
  by (cases op; auto)

lemma bin_node_nonode:
  "bin_node op x y ≠ NoNode"
  by (cases op; auto)

theorem term_graph_reconstruction:
  "g ⊕ e ↝ (g', n) ⟹ (g' ⊢ n ≃ e) ∧ as_set g ⊆ as_set g'"
  subgoal premises e apply (rule conjI) defer
    using e unrep_subset apply blast using e
  proof (induction g e "(g', n)" arbitrary: g' n)
    case (UnrepConstantNode g c g⇩1 n)
    then show ?case 
      using ConstantNode unique_kind by blast
  next
    case (UnrepParameterNode g i s g⇩1 n)
    then show ?case 
      using ParameterNode unique_kind
      by (metis IRNode.distinct(3695))
  next
    case (UnrepConditionalNode g ce g⇩1 c te g⇩2 t fe g⇩3 f s' g⇩4 n)
    then show ?case 
      using unique_kind unique_eval unrep_eval
      by (meson ConditionalNode IRNode.distinct(965))
  next
    case (UnrepUnaryNode g xe g⇩1 x s' op g⇩2 n)
    then have k: "kind g⇩2 n = unary_node op x"
      using unique_kind unary_node_nonode by simp
    then have "g⇩2 ⊢ x ≃ xe"
      using UnrepUnaryNode unique_eval by blast
    then show ?case 
      using k apply (cases op)
      using unary_node.simps(1,2,3,4,5,6,7,8,9,10)
            AbsNode NegateNode NotNode LogicNegationNode NarrowNode SignExtendNode ZeroExtendNode 
            IsNullNode ReverseBytesNode BitCountNode
      by presburger+
  next
    case (UnrepBinaryNode g xe g⇩1 x ye g⇩2 y s' op g⇩3 n)
    then have k: "kind g⇩3 n = bin_node op x y"
      using unique_kind bin_node_nonode by simp
    have x: "g⇩3 ⊢ x ≃ xe" 
      using UnrepBinaryNode unique_eval unrep_eval by blast
    have y: "g⇩3 ⊢ y ≃ ye" 
      using UnrepBinaryNode unique_eval unrep_eval by blast
    then show ?case 
      using x k apply (cases op)
      using bin_node.simps(1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18)
            AddNode MulNode DivNode ModNode SubNode AndNode OrNode ShortCircuitOrNode LeftShiftNode RightShiftNode 
            UnsignedRightShiftNode IntegerEqualsNode IntegerLessThanNode IntegerBelowNode XorNode
            IntegerTestNode IntegerNormalizeCompareNode IntegerMulHighNode
      by metis+
  next
    case (AllLeafNodes g n s)
    then show ?case 
      by (simp add: rep.LeafNode)
  qed
  done

lemma ref_refinement:
  assumes "g ⊢ n ≃ e⇩1"
  assumes "kind g n' = RefNode n"
  shows "g ⊢ n' ⊴ e⇩1"
  by (meson equal_refines graph_represents_expression_def RefNode assms)

lemma unrep_refines:
  assumes "g ⊕ e ↝ (g', n)"
  shows "graph_refinement g g'"
  using assms by (simp add: unrep_subset subset_refines)

lemma add_new_node_refines:
  assumes "n ∉ ids g"
  assumes "g' = add_node n (k, s) g"
  shows "graph_refinement g g'"
  using assms by (simp add: fresh_node_subset subset_refines)

lemma add_node_as_set:
  assumes "g' = add_node n (k, s) g"
  shows "({n} ⊴ as_set g) ⊆ as_set g'"
  unfolding assms
  by (smt (verit, ccfv_SIG) case_prodE changeonly.simps mem_Collect_eq prod.sel(1) subsetI assms
      add_changed as_set_def domain_subtraction_def)

theorem refined_insert:
  assumes "e⇩1 ≥ e⇩2"
  assumes "g⇩1 ⊕ e⇩2 ↝ (g⇩2, n')"
  shows "(g⇩2 ⊢ n' ⊴ e⇩1) ∧ graph_refinement g⇩1 g⇩2"
  using assms graph_construction term_graph_reconstruction by blast

lemma ids_finite: "finite (ids g)"
  by simp

lemma unwrap_sorted: "set (sorted_list_of_set (ids g)) = ids g"
  using ids_finite by simp

lemma find_none:
  assumes "find_node_and_stamp g (k, s) = None"
  shows "∀ n ∈ ids g. kind g n ≠ k ∨ stamp g n ≠ s"
proof -
  have "(∄n. n ∈ ids g ∧ (kind g n = k ∧ stamp g n = s))"
    by (metis (mono_tags) unwrap_sorted find_None_iff find_node_and_stamp.simps assms)
  then show ?thesis
    by auto
qed

(*

section ‹An attempt at a constructive refinement proof›
lemma add_node_ids_subset:
  assumes "n ∈ ids g"
  assumes "g' = add_node n node g"
  shows "ids g' = ids g ∪ {n}"
  using assms unfolding add_node_def
  apply (cases "fst node = NoNode") 
  using ids.rep_eq replace_node.rep_eq replace_node_def apply auto[1]
  unfolding ids_def
  by (smt (verit, best) Collect_cong Un_insert_right dom_fun_upd fst_conv fun_upd_apply ids.rep_eq ids_def insert_absorb mem_Collect_eq option.inject option.simps(3) replace_node.rep_eq replace_node_def sup_bot.right_neutral)
  
theorem constructive_refinement:
  assumes 1: "e⇩1 ≥ e⇩2"
  assumes "g⇩1 ⊢ n ≃ e⇩1"
  assumes "g⇩1 ⊕ e⇩2 ↝ (g⇩2, n')"
  assumes "n ≠ n'"
  assumes "g⇩3 = add_node n (RefNode n', stamp g⇩2 n') g⇩2"
  shows "graph_refinement g⇩1 g⇩3"
proof -
  have step1: "graph_refinement g⇩1 g⇩2"
    using assms(2,3)
    by (simp add: subset_refines unrep_subset)
  have "n ∈ ids g⇩2"
    using assms(2) assms(3) no_encoding unrep_unchanged by blast
  then have "ids g⇩2 = ids g⇩3"
    using assms(5) add_node_ids_subset
    by blast
  have 3: "g⇩2 ⊢ n ≃ e⇩1"
    using assms(3)
    using assms(2) subset_implies_evals unrep_subset by blast
  then have g2rep1: "g⇩2 ⊢ n ⊴ e⇩1"
    using 1 unfolding graph_represents_expression_def
    by blast
  have g2rep: "g⇩2 ⊢ n' ⊴ e⇩1"
    using assms(3) term_graph_reconstruction
    using "1" graph_construction by blast
  have 2: "({n} ⊴ as_set g⇩2) ⊆ as_set g⇩3"
    using assms(5) add_node_as_set by blast
  have "kind g⇩3 n = RefNode n'"
    using assms(5) find_new_kind by blast
  have g3rep: "(g⇩3 ⊢ n' ⊴ e⇩1)"
    using g2rep1 g2rep assms(4) 2 
    (*by (meson ‹kind g⇩3 n = RefNode n'› assms(5) graph_represents_expression_def rep_ref)*)
  have refkind: "kind g⇩3 n = RefNode n'"
    using assms(5) add_node_lookup
    by (metis IRNode.distinct(2755))
  then have 4: "g⇩3 ⊢ n ⊴ e⇩1"
    using assms
    using RefNode g3rep
    by (meson graph_represents_expression_def)
  have step2: "graph_refinement g⇩2 g⇩3"
    using graph_semantics_preservation 1 2 3 4
    by (meson graph_represents_expression_def order_trans)
  from step1 step2 show ?thesis
    by (meson assms(3) graph_refinement_def order_trans subsetD subset_implies_evals unrep_subset)
qed
*)





(*
lemma
  assumes "maximal_sharing g⇩1"
  assumes "e⇩1 ≥ e⇩2"
  assumes "g⇩1 ⊕ e⇩2 ↝ (g⇩2, n')"
  shows "maximal_sharing g⇩2"
  using assms(3,1)
  apply (induction g⇩1 e⇩2 "(g⇩2, n')" arbitrary: g⇩2 n') 
  apply blast using find_none sorry
*)


(*
lemma
  assumes "maximal_sharing g"
  assumes "g ⊕ e ↝ (g', n)"
  shows "∀n' . n' ∈ ids g' - ids g ⟶ 
         (∀e . (g' ⊢ n' ≃ e) ⟶ 
          ¬(∃n'' . n'' ∈ true_ids g' ∧ n'' = n' ∧ (g' ⊢ n'' ≃ e)))"
  using assms(2)
  apply (induction g e "(g', n)" arbitrary: g' n) 
  apply blast sorry

lemma
  "maximal_sharing g ⟹ g ⊕ e ↝ (g', n) ⟹ maximal_sharing g'"
  sorry

lemma only_n_changes:
  assumes "({n} ⊴ as_set g) ⊆ as_set g'"
  shows "∀n'. n' ∈ ids g - {n} ⟶ (∀e. (g ⊢ n' ≃ e) ⟶ (g' ⊢ n' ≃ e))"
  apply (rule allI) apply (rule impI)
  subgoal premises set for n' apply (rule allI) apply (rule impI)
    subgoal premises eval for e
      using eval set assms proof (induction n' e )
      case (ConstantNode n c)
      then show ?case
        by (metis Diff_iff not_excluded_keep_type rep.ConstantNode)
    next
      case (ParameterNode n i s)
      then show ?case
        by (metis DiffD1 DiffD2 not_excluded_keep_type rep.ParameterNode)
    next
      case (ConditionalNode n c t f ce te fe)
      then show ?case sorry
    next
      case (AbsNode n x xe)
      then show ?case sorry
    next
      case (NotNode n x xe)
      then show ?case sorry
    next
      case (NegateNode n x xe)
      then show ?case sorry
    next
      case (LogicNegationNode n x xe)
      then show ?case sorry
    next
      case (AddNode n x y xe ye)
      then show ?case sorry
    next
      case (MulNode n x y xe ye)
      then show ?case sorry
    next
      case (SubNode n x y xe ye)
      then show ?case sorry
    next
      case (AndNode n x y xe ye)
      then show ?case sorry
    next
      case (OrNode n x y xe ye)
      then show ?case sorry
    next
      case (XorNode n x y xe ye)
      then show ?case sorry
    next
      case (LeftShiftNode n x y xe ye)
      then show ?case sorry
    next
      case (RightShiftNode n x y xe ye)
      then show ?case sorry
    next
      case (UnsignedRightShiftNode n x y xe ye)
      then show ?case sorry
    next
      case (IntegerBelowNode n x y xe ye)
      then show ?case sorry
    next
      case (IntegerEqualsNode n x y xe ye)
      then show ?case sorry
    next
      case (IntegerLessThanNode n x y xe ye)
      then show ?case sorry
    next
      case (NarrowNode n inputBits resultBits x xe)
      then show ?case sorry
    next
      case (SignExtendNode n inputBits resultBits x xe)
      then show ?case sorry
    next
      case (ZeroExtendNode n inputBits resultBits x xe)
      then show ?case sorry
    next
      case (LeafNode n s)
      then show ?case sorry
    next
      case (RefNode n n' e)
      then show ?case sorry
    qed
     
      apply (metis ConstantNode DiffE not_excluded_keep_type)
      apply (metis DiffD1 DiffD2 ParameterNode not_excluded_keep_type) sorry
  proof -
    have "kind g n' = kind g' n'"
      using assms set
      by (meson Diff_iff not_excluded_keep_type)
    moreover have "stamp g n' = stamp g' n'"
      using assms set
      by (meson DiffE not_excluded_keep_type)
    ultimately show "∀e. (g ⊢ n' ≃ e) ⟶ (g' ⊢ n' ≃ e)"
      using assms sorry
  qed
  done*)

method ref_represents uses node =
  (metis IRNode.distinct(2755) RefNode dual_order.refl find_new_kind fresh_node_subset node subset_implies_evals)

(*
lemma
  assumes "kind g n = RefNode n'"
  assumes "g ⊢ n ≃ e"
  assumes "n ≠ n'"
  shows "n ∉ eval_usages g n'"
  using assms(2,1,3) apply (induction e arbitrary: n; auto) sorry


lemma unaffected_rep:
  assumes "({n} ⊴ as_set g) ⊆ as_set g'"
  assumes "g ⊢ n' ≃ e"
  assumes "n ∉ eval_usages g n'"
  shows "g' ⊢ n' ≃ e"
  using assms(2)
proof -
  have ne: "n ≠ n'"
    using assms(3)
    using assms(2) eval_contains_id eval_usages_self by blast
  show ?thesis 
    using assms(2) assms ne apply (induction e) using ne 
                        apply (metis ConstantNode encodes_contains not_excluded_keep_type not_in_g singleton_iff)
                      apply (metis ParameterNode empty_iff encode_in_ids insertE not_excluded_keep_type)
    sorry
qed

lemma ref_add_represents:
  assumes "g ⊢ n ⊴ e"
  assumes "g ⊢ n' ⊴ e"
  assumes "g' = add_node n' (RefNode n, s) g"
  assumes "n' ∉ eval_usages g n"
  shows "g' ⊢ n' ⊴ e" using assms
  by (metis IRNode.distinct(2755) RefNode add_node_as_set find_new_kind graph_represents_expression_def unaffected_rep)
(*proof -
  have as_set: "({n'} ⊴ as_set g) ⊆ as_set g'"
    using assms(3)
    by (simp add: add_node_as_set)
  have "kind g' n' = RefNode n"
    using assms(3)
    using find_new_kind by blast
  show ?thesis unfolding graph_represents_expression_def 
  proof -
    obtain e' where e'def: "(g ⊢ n ≃ e') ∧ e ≥ e'"
      using assms(1) graph_represents_expression_def by blast
    then obtain e2' where "g' ⊢ n ≃ e2'"
      using as_set using unaffected_rep
      using assms(4) by blast
    obtain e'' where e''def: "(g ⊢ n' ≃ e'') ∧ e ≥ e''"
      using assms(2) graph_represents_expression_def by blast
    have "g' ⊢ n' ≃ e''"
      using as_set e''def sorry
    show "∃e'. (g' ⊢ n' ≃ e') ∧ e ≥ e'"
   sorry
   sorry
                      (*apply (ref_represents node: rep.ConstantNode)
                      apply (ref_represents node: rep.ParameterNode)
                      apply (ref_represents node: rep.ConditionalNode)
                      apply (ref_represents node: rep.AbsNode)
                     apply (ref_represents node: rep.NotNode)
                    apply (ref_represents node: rep.NegateNode)
                   apply (ref_represents node: rep.LogicNegationNode)
                  apply (ref_represents node: rep.AddNode)
                 apply (ref_represents node: rep.MulNode)
                apply (ref_represents node: rep.SubNode)
               apply (ref_represents node: rep.AndNode)
              apply (ref_represents node: rep.OrNode)
             apply (ref_represents node: rep.XorNode)
            apply (ref_represents node: rep.LeftShiftNode)
           apply (ref_represents node: rep.RightShiftNode)
          apply (ref_represents node: rep.UnsignedRightShiftNode)
         apply (ref_represents node: rep.IntegerBelowNode)
        apply (ref_represents node: rep.IntegerEqualsNode)
       apply (ref_represents node: rep.IntegerLessThanNode)
      apply (ref_represents node: rep.NarrowNode)
     apply (ref_represents node: rep.SignExtendNode)
    apply (ref_represents node: rep.ZeroExtendNode)
   apply (ref_represents node: rep.LeafNode)
  by (ref_represents node: rep.RefNode)*)
*)

theorem constructive_refinement:
  assumes 1: "e⇩1 ≥ e⇩2"
  assumes "g⇩1 ⊢ n ≃ e⇩1"
  assumes "g⇩1 ◃ e⇩2 ↝ (g⇩2, n')"
  assumes "n ≠ n'"
  assumes "g⇩3 = add_node n (RefNode n', stamp g⇩2 n') g⇩2"
  shows "graph_refinement g⇩1 g⇩3"
proof -
  have step1: "graph_refinement g⇩1 g⇩2"
    using assms(2,3)
    by (simp add: subset_refines unrep_subset)
  have "ids g⇩2 ⊆ ids g⇩3"
    using assms(5)
    by (metis (no_types, lifting) IRNode.distinct(2755) add_node_def assms(2) assms(3) find_new_kind ids_some insertE insert_Diff no_encoding replace_node_def replace_node_unchanged subsetI unrep_unchanged)
  have 3: "g⇩2 ⊢ n ≃ e⇩1"
    using assms(3)
    using assms(2) subset_implies_evals unrep_subset by blast
  then have g2rep1: "g⇩2 ⊢ n ⊴ e⇩1"
    using 1 unfolding graph_represents_expression_def
    by blast
  have g2rep: "g⇩2 ⊢ n' ⊴ e⇩1"
    using assms(3) term_graph_reconstruction
    using "1" graph_construction by blast
  have 2: "({n} ⊴ as_set g⇩2) ⊆ as_set g⇩3"
    using assms(5) add_node_as_set by blast
  have "kind g⇩3 n = RefNode n'"
    using assms(5) find_new_kind by blast
  have g3rep: "(g⇩3 ⊢ n' ⊴ e⇩1)"
    using g2rep1 g2rep assms(4) 2 ref_add_represents g2rep1 sorry
    (*by (meson ‹kind g⇩3 n = RefNode n'› assms(5) graph_represents_expression_def rep_ref)*)
  have refkind: "kind g⇩3 n = RefNode n'"
    using assms(5) add_node_lookup
    by (metis IRNode.distinct(2755))
  then have 4: "g⇩3 ⊢ n ⊴ e⇩1"
    using assms
    using RefNode g3rep
    by (meson graph_represents_expression_def)
  have step2: "graph_refinement g⇩2 g⇩3"
    using graph_semantics_preservation 1 2 3 4
    by (meson graph_represents_expression_def order_trans)
  from step1 step2 show ?thesis
    by (meson assms(3) graph_refinement_def order_trans subsetD subset_implies_evals unrep_subset)
qed
*)

subsubsection ‹Data-flow Tree to Subgraph Preserves Maximal Sharing›

lemma same_kind_stamp_encodes_equal:
  assumes "kind g n = kind g n'"
  assumes "stamp g n = stamp g n'"
  assumes "¬(is_preevaluated (kind g n))"
  shows "∀ e. (g ⊢ n ≃ e) ⟶ (g ⊢ n' ≃ e)"
  apply (rule allI)
  subgoal for e
    apply (rule impI)
    subgoal premises eval using eval assms
      apply (induction e)
    using ConstantNode apply presburger
    using ParameterNode apply presburger 
                        apply (metis ConditionalNode)
                        apply (metis AbsNode)
                        apply (metis ReverseBytesNode)
                        apply (metis BitCountNode)
                       apply (metis NotNode)
                      apply (metis NegateNode)
                     apply (metis LogicNegationNode)
                    apply (metis AddNode)
                    apply (metis MulNode)
                   apply (metis DivNode)
                  apply (metis ModNode)
                  apply (metis SubNode)
                 apply (metis AndNode)
                apply (metis OrNode)
                apply (metis XorNode)
                apply (metis ShortCircuitOrNode)
              apply (metis LeftShiftNode)
             apply (metis RightShiftNode)
            apply (metis UnsignedRightShiftNode)
           apply (metis IntegerBelowNode)
          apply (metis IntegerEqualsNode)
         apply (metis IntegerLessThanNode)
          apply (metis IntegerTestNode)
        apply (metis IntegerNormalizeCompareNode)
        apply (metis IntegerMulHighNode)
        apply (metis NarrowNode)
       apply (metis SignExtendNode)
      apply (metis ZeroExtendNode)
    defer
     apply (metis PiNode)
   apply (metis RefNode) 
  apply (metis IsNullNode)
  by blast
    done
  done

lemma new_node_not_present:
  assumes "find_node_and_stamp g (node, s) = None"
  assumes "n = get_fresh_id g"
  assumes "g' = add_node n (node, s) g"
  shows "∀ n' ∈ true_ids g. (∀e. ((g ⊢ n ≃ e) ∧ (g ⊢ n' ≃ e)) ⟶ n = n')"
  using assms encode_in_ids fresh_ids by blast

lemma true_ids_def:
  "true_ids g = {n ∈ ids g. ¬(is_RefNode (kind g n)) ∧ ((kind g n) ≠ NoNode)}"
  using true_ids_def by (auto simp add: is_RefNode_def)

lemma add_node_some_node_def:
  assumes "k ≠ NoNode"
  assumes "g' = add_node nid (k, s) g"
  shows "g' = Abs_IRGraph ((Rep_IRGraph g)(nid ↦ (k, s)))"
  by (metis Rep_IRGraph_inverse add_node.rep_eq fst_conv assms)

lemma ids_add_update_v1:
  assumes "g' = add_node nid (k, s) g"
  assumes "k ≠ NoNode"
  shows "dom (Rep_IRGraph g') = dom (Rep_IRGraph g) ∪ {nid}"
  by (simp add: add_node.rep_eq assms)

lemma ids_add_update_v2:
  assumes "g' = add_node nid (k, s) g"
  assumes "k ≠ NoNode"
  shows "nid ∈ ids g'"
  by (simp add: find_new_kind assms)

lemma add_node_ids_subset:
  assumes "n ∈ ids g"
  assumes "g' = add_node n node g"
  shows "ids g' = ids g ∪ {n}"
  using assms replace_node.rep_eq by (auto simp add: replace_node_def ids.rep_eq add_node_def)

lemma convert_maximal:
  assumes "∀n n'. n ∈ true_ids g ∧ n' ∈ true_ids g ⟶ 
          (∀e e'. (g ⊢ n ≃ e) ∧ (g ⊢ n' ≃ e') ⟶ e ≠ e')"
  shows "maximal_sharing g"
  using assms by (auto simp add: maximal_sharing)

lemma add_node_set_eq:
  assumes "k ≠ NoNode"
  assumes "n ∉ ids g"
  shows "as_set (add_node n (k, s) g) = as_set g ∪ {(n, (k, s))}"
  using assms unfolding as_set_def by (transfer; auto)

lemma add_node_as_set_eq:
  assumes "g' = add_node n (k, s) g"
  assumes "n ∉ ids g"
  shows "({n} ⊴ as_set g') = as_set g"
  unfolding domain_subtraction_def
  by (smt (z3) assms add_node_set_eq Collect_cong Rep_IRGraph_inverse UnCI add_node.rep_eq le_boolE
      as_set_def case_prodE2 case_prodI2 le_boolI' mem_Collect_eq prod.sel(1) singletonD singletonI
      UnE)

lemma true_ids:
  "true_ids g = ids g - {n ∈ ids g. is_RefNode (kind g n)}"
  unfolding true_ids_def by fastforce

lemma as_set_ids:
  assumes "as_set g = as_set g'"
  shows "ids g = ids g'"
  by (metis antisym equalityD1 graph_refinement_def subset_refines assms)

lemma ids_add_update:
  assumes "k ≠ NoNode"
  assumes "n ∉ ids g"
  assumes "g' = add_node n (k, s) g"
  shows "ids g' = ids g ∪ {n}"
  by (smt (z3) Diff_idemp Diff_insert_absorb Un_commute add_node.rep_eq insert_is_Un insert_Collect
      add_node_def ids.rep_eq ids_add_update_v1 insertE assms replace_node_unchanged Collect_cong
      map_upd_Some_unfold mem_Collect_eq replace_node_def ids_add_update_v2)

lemma true_ids_add_update:
  assumes "k ≠ NoNode"
  assumes "n ∉ ids g"
  assumes "g' = add_node n (k, s) g"
  assumes "¬(is_RefNode k)"
  shows "true_ids g' = true_ids g ∪ {n}" 
  by (smt (z3) Collect_cong Diff_iff Diff_insert_absorb Un_commute add_node_def find_new_kind assms
     insert_Diff_if insert_is_Un mem_Collect_eq replace_node_def replace_node_unchanged true_ids
     ids_add_update)

lemma new_def:
  assumes "(new ⊴ as_set g') = as_set g"
  shows "n ∈ ids g ⟶ n ∉ new"
  using assms apply auto unfolding as_set_def
  by (smt (z3) as_set_def case_prodD domain_subtraction_def mem_Collect_eq assms ids_some)

lemma add_preserves_rep:
  assumes unchanged: "(new ⊴ as_set g') = as_set g"
  assumes closed: "wf_closed g"
  assumes existed: "n ∈ ids g"
  assumes "g' ⊢ n ≃ e"
  shows "g ⊢ n ≃ e"
proof (cases "n ∈ new")
  case True
  have "n ∉ ids g"
    using unchanged True as_set_def unfolding domain_subtraction_def by blast
  then show ?thesis 
    using existed by simp
next
  case False
  have kind_eq: "∀ n' . n' ∉ new ⟶ kind g n' = kind g' n'"
    ―‹can be more general than $stamp\_eq$ because NoNode default is equal›
    apply (rule allI; rule impI)
    by (smt (z3) case_prodE domain_subtraction_def ids_some mem_Collect_eq subsetI unchanged
        not_excluded_keep_type)
  from False have stamp_eq: "∀ n' ∈ ids g' . n' ∉ new ⟶ stamp g n' = stamp g' n'"
    by (metis equalityE not_excluded_keep_type unchanged)
  show ?thesis 
    using assms(4) kind_eq stamp_eq False
  proof (induction n e rule: rep.induct)
    case (ConstantNode n c)
    then show ?case
      by (simp add: rep.ConstantNode)
  next
    case (ParameterNode n i s)
    then show ?case
      by (metis no_encoding rep.ParameterNode)
  next
    case (ConditionalNode n c t f ce te fe)
    have kind: "kind g n = ConditionalNode c t f"
      by (simp add: kind_eq ConditionalNode.prems(3) ConditionalNode.hyps(1))
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{c, t, f} = inputs g n"
      by (simp add: kind)
    have "c ∈ ids g ∧ t ∈ ids g ∧ f ∈ ids g"
      using closed wf_closed_def isin inputs by blast
    then have "c ∉ new ∧ t ∉ new ∧ f ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case 
      by (simp add: rep.ConditionalNode ConditionalNode)
  next
    case (AbsNode n x xe)
    then have kind: "kind g n = AbsNode x"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{x} = inputs g n"
      by (simp add: kind)
    have "x ∈ ids g"
      using closed wf_closed_def isin inputs by blast
    then have "x ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case
      by (simp add: AbsNode rep.AbsNode)
  next
    case (ReverseBytesNode n x xe)
    then have kind: "kind g n = ReverseBytesNode x"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{x} = inputs g n"
      by (simp add: kind)
    have "x ∈ ids g"
      using closed wf_closed_def isin inputs by blast
    then have "x ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case
      using ReverseBytesNode.IH kind kind_eq rep.ReverseBytesNode stamp_eq by blast
  next
    case (BitCountNode n x xe)
    then have kind: "kind g n = BitCountNode x"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{x} = inputs g n"
      by (simp add: kind)
    have "x ∈ ids g"
      using closed wf_closed_def isin inputs by blast
    then have "x ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case
      using BitCountNode.IH kind kind_eq rep.BitCountNode stamp_eq by blast
  next
    case (NotNode n x xe)
    then have kind: "kind g n = NotNode x"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{x} = inputs g n"
      by (simp add: kind)
    have "x ∈ ids g"
      using closed wf_closed_def isin inputs by blast
    then have "x ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case 
      by (simp add: NotNode rep.NotNode)
  next
    case (NegateNode n x xe)
    then have kind: "kind g n = NegateNode x"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{x} = inputs g n"
      by (simp add: kind)
    have "x ∈ ids g"
      using closed  wf_closed_def isin inputs by blast
    then have "x ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case 
      by (simp add: NegateNode rep.NegateNode)
  next
    case (LogicNegationNode n x xe)
    then have kind: "kind g n = LogicNegationNode x"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{x} = inputs g n"
      by (simp add: kind)
    have "x ∈ ids g"
      using closed wf_closed_def isin inputs by blast
    then have "x ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case 
      by (simp add: LogicNegationNode rep.LogicNegationNode)
  next
    case (AddNode n x y xe ye)
    then have kind: "kind g n = AddNode x y"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{x, y} = inputs g n"
      by (simp add: kind)
    have "x ∈ ids g ∧ y ∈ ids g"
      using closed wf_closed_def isin inputs by blast
    then have "x ∉ new ∧ y ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case 
      by (simp add: AddNode rep.AddNode)
  next
    case (MulNode n x y xe ye)
    then have kind: "kind g n = MulNode x y"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{x, y} = inputs g n"
      by (simp add: kind)
    have "x ∈ ids g ∧ y ∈ ids g"
      using closed wf_closed_def isin inputs by blast
    then have "x ∉ new ∧ y ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case 
      by (simp add: MulNode rep.MulNode)
  next
    case (DivNode n x y xe ye)
    then have kind: "kind g n = SignedFloatingIntegerDivNode x y"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{x, y} = inputs g n"
      by (simp add: kind)
    have "x ∈ ids g ∧ y ∈ ids g"
      using closed wf_closed_def isin inputs by blast
    then have "x ∉ new ∧ y ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case 
      by (simp add: DivNode rep.DivNode)
  next
    case (ModNode n x y xe ye)
    then have kind: "kind g n = SignedFloatingIntegerRemNode x y"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{x, y} = inputs g n"
      by (simp add: kind)
    have "x ∈ ids g ∧ y ∈ ids g"
      using closed wf_closed_def isin inputs by blast
    then have "x ∉ new ∧ y ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case 
      by (simp add: ModNode rep.ModNode)
  next
    case (SubNode n x y xe ye)
    then have kind: "kind g n = SubNode x y"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{x, y} = inputs g n"
      by (simp add: kind)
    have "x ∈ ids g ∧ y ∈ ids g"
      using closed wf_closed_def isin inputs by blast
    then have "x ∉ new ∧ y ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case 
      by (simp add: SubNode rep.SubNode)
  next
    case (AndNode n x y xe ye)
    then have kind: "kind g n = AndNode x y"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{x, y} = inputs g n"
      by (simp add: kind)
    have "x ∈ ids g ∧ y ∈ ids g"
      using closed wf_closed_def isin inputs by blast
    then have "x ∉ new ∧ y ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case 
      by (simp add: AndNode rep.AndNode)
  next
    case (OrNode n x y xe ye)
    then have kind: "kind g n = OrNode x y"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{x, y} = inputs g n"
      by (simp add: kind)
    have "x ∈ ids g ∧ y ∈ ids g"
      using closed wf_closed_def isin inputs by blast
    then have "x ∉ new ∧ y ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case 
      by (simp add: OrNode rep.OrNode)
  next
    case (XorNode n x y xe ye)
    then have kind: "kind g n = XorNode x y"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{x, y} = inputs g n"
      by (simp add: kind)
    have "x ∈ ids g ∧ y ∈ ids g"
      using closed wf_closed_def isin inputs by blast
    then have "x ∉ new ∧ y ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case 
      by (simp add: XorNode rep.XorNode)
  next
    case (ShortCircuitOrNode n x y xe ye)
    then have kind: "kind g n = ShortCircuitOrNode x y"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{x, y} = inputs g n"
      by (simp add: kind)
    have "x ∈ ids g ∧ y ∈ ids g"
      using closed wf_closed_def isin inputs by blast
    then have "x ∉ new ∧ y ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case 
      by (simp add: ShortCircuitOrNode rep.ShortCircuitOrNode)
  next
    case (LeftShiftNode n x y xe ye)
    then have kind: "kind g n = LeftShiftNode x y"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{x, y} = inputs g n"
      by (simp add: kind)
    have "x ∈ ids g ∧ y ∈ ids g"
      using closed wf_closed_def isin inputs by blast
    then have "x ∉ new ∧ y ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case 
      by (simp add: LeftShiftNode rep.LeftShiftNode)
  next
    case (RightShiftNode n x y xe ye)
    then have kind: "kind g n = RightShiftNode x y"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{x, y} = inputs g n"
      by (simp add: kind)
    have "x ∈ ids g ∧ y ∈ ids g"
      using closed wf_closed_def isin inputs by blast
    then have "x ∉ new ∧ y ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case 
      by (simp add: RightShiftNode rep.RightShiftNode)
  next
    case (UnsignedRightShiftNode n x y xe ye)
    then have kind: "kind g n = UnsignedRightShiftNode x y"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{x, y} = inputs g n"
      by (simp add: kind)
    have "x ∈ ids g ∧ y ∈ ids g"
      using closed wf_closed_def isin inputs by blast
    then have "x ∉ new ∧ y ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case 
      by (simp add: UnsignedRightShiftNode rep.UnsignedRightShiftNode)
  next
    case (IntegerBelowNode n x y xe ye)
    then have kind: "kind g n = IntegerBelowNode x y"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{x, y} = inputs g n"
      by (simp add: kind)
    have "x ∈ ids g ∧ y ∈ ids g"
      using closed wf_closed_def isin inputs by blast
    then have "x ∉ new ∧ y ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case 
      by (simp add: IntegerBelowNode rep.IntegerBelowNode)
  next
    case (IntegerEqualsNode n x y xe ye)
    then have kind: "kind g n = IntegerEqualsNode x y"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{x, y} = inputs g n"
      by (simp add: kind)
    have "x ∈ ids g ∧ y ∈ ids g"
      using closed wf_closed_def isin inputs by blast
    then have "x ∉ new ∧ y ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case 
      by (simp add: IntegerEqualsNode rep.IntegerEqualsNode)
  next
    case (IntegerLessThanNode n x y xe ye)
    then have kind: "kind g n = IntegerLessThanNode x y"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{x, y} = inputs g n"
      by (simp add: kind)
    have "x ∈ ids g ∧ y ∈ ids g"
      using closed wf_closed_def isin inputs by blast
    then have "x ∉ new ∧ y ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case 
      by (simp add: IntegerLessThanNode rep.IntegerLessThanNode)
  next
    case (IntegerTestNode n x y xe ye)
    then have kind: "kind g n = IntegerTestNode x y"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{x, y} = inputs g n"
      by (simp add: kind)
    have "x ∈ ids g ∧ y ∈ ids g"
      using closed wf_closed_def isin inputs by blast
    then have "x ∉ new ∧ y ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case 
      by (simp add: IntegerTestNode rep.IntegerTestNode)
  next
    case (IntegerNormalizeCompareNode n x y xe ye)
    then have kind: "kind g n = IntegerNormalizeCompareNode x y"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{x, y} = inputs g n"
      by (simp add: kind)
    have "x ∈ ids g ∧ y ∈ ids g"
      using closed wf_closed_def isin inputs by blast
    then have "x ∉ new ∧ y ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case
      using IntegerNormalizeCompareNode.IH(1,2) kind kind_eq rep.IntegerNormalizeCompareNode
            stamp_eq by blast
  next
    case (IntegerMulHighNode n x y xe ye)
    then have kind: "kind g n = IntegerMulHighNode x y"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{x, y} = inputs g n"
      by (simp add: kind)
    have "x ∈ ids g ∧ y ∈ ids g"
      using closed wf_closed_def isin inputs by blast
    then have "x ∉ new ∧ y ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case
      using IntegerMulHighNode.IH(1,2) kind kind_eq rep.IntegerMulHighNode stamp_eq by blast
  next
    case (NarrowNode n inputBits resultBits x xe)
    then have kind: "kind g n = NarrowNode inputBits resultBits x"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{x} = inputs g n"
      by (simp add: kind)
    have "x ∈ ids g"
      using closed wf_closed_def isin inputs by blast
    then have "x ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case 
      by (simp add: NarrowNode rep.NarrowNode)
  next
    case (SignExtendNode n inputBits resultBits x xe)
    then have kind: "kind g n = SignExtendNode inputBits resultBits x"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{x} = inputs g n"
      by (simp add: kind)
    have "x ∈ ids g"
      using closed wf_closed_def isin inputs by blast
    then have "x ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case 
      by (simp add: SignExtendNode rep.SignExtendNode)
  next
    case (ZeroExtendNode n inputBits resultBits x xe)
    then have kind: "kind g n = ZeroExtendNode inputBits resultBits x"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{x} = inputs g n"
      by (simp add: kind)
    have "x ∈ ids g"
      using closed wf_closed_def isin inputs by blast
    then have "x ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case 
      by (simp add: ZeroExtendNode rep.ZeroExtendNode)
  next
    case (LeafNode n s)
    then show ?case
      by (metis no_encoding rep.LeafNode)
  next
    case (PiNode n n' gu e)
    then have kind: "kind g n = PiNode n' gu"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "set (n' # (opt_to_list gu)) = inputs g n"
      by (simp add: kind)
    have "n' ∈ ids g"
      by (metis in_mono list.set_intros(1) inputs isin wf_closed_def closed)
    then show ?case
      using PiNode.IH kind kind_eq new_def rep.PiNode stamp_eq unchanged by blast
  next
    case (RefNode n n' e)
    then have kind: "kind g n = RefNode n'"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{n'} = inputs g n"
      by (simp add: kind)
    have "n' ∈ ids g"
      using closed wf_closed_def isin inputs by blast
    then have "n' ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case
      by (simp add: RefNode rep.RefNode)
  next
    case (IsNullNode n v)
    then have kind: "kind g n = IsNullNode v"
      by simp
    then have isin: "n ∈ ids g"
      by simp
    have inputs: "{v} = inputs g n"
      by (simp add: kind)
    have "v ∈ ids g"
      using closed wf_closed_def isin inputs by blast
    then have "v ∉ new"
      using unchanged by (simp add: new_def)
    then show ?case 
      by (simp add: rep.IsNullNode stamp_eq kind_eq kind IsNullNode.IH)
  qed 
qed

lemma not_in_no_rep:
  "n ∉ ids g ⟹ ∀e. ¬(g ⊢ n ≃ e)"
  using eval_contains_id by auto

(*
lemma insert_maximal_sharing:
  assumes "k ≠ NoNode ∧ ¬(is_RefNode k)"
  assumes "find_node_and_stamp g (k, s) = None"
  assumes "n = get_fresh_id g"
  assumes "g' = add_node n (k, s) g"
  assumes "g' ⊢ n ≃ e"
  assumes "wf_closed g"
  assumes "maximal_sharing g"
  shows "maximal_sharing g'"
using assms proof -
  have "kind g' n = k"
    using assms find_new_kind by blast
  have "¬(is_RefNode k) ∧ k ≠ NoNode"
    using assms(1) by simp
  then have dom: "true_ids g' = true_ids g ∪ {n}"
    using assms(3) assms(4) fresh_ids true_ids_add_update by presburger
  have new: "n ∉ ids g"
    using fresh_ids
    using assms(3) by presburger
  obtain new where "new = true_ids g' - true_ids g"
    by simp
  then have new_def: "new = {n}"
    by (metis (no_types, lifting) DiffE Diff_cancel IRGraph.true_ids_def Un_insert_right dom insert_Diff_if new sup_bot_right)
  then have unchanged: "(new ⊴ as_set g') = as_set g"
    using add_node_as_set_eq assms(4) new by presburger
  then have kind_eq: "∀n' . n' ∉ new ⟶ kind g n' = kind g' n'"
    by (metis add_node_as_set assms(4) local.new_def not_excluded_keep_type not_in_g order_class.order_eq_iff)
  from unchanged have stamp_eq: "∀n' ∈ ids g . n' ∉ new ⟶ stamp g n' = stamp g' n'"
    using not_excluded_keep_type new_def new
    by (metis add_node_as_set assms(4))
  show ?thesis unfolding maximal_sharing apply (rule allI; rule allI; rule impI)
  using assms(7) unfolding maximal_sharing apply auto
  proof -
    fix n⇩1 n⇩2 e
    assume 1: "∀n⇩1 n⇩2.
          n⇩1 ∈ true_ids g ∧ n⇩2 ∈ true_ids g ⟶
          (∃e. (g ⊢ n⇩1 ≃ e) ∧ (g ⊢ n⇩2 ≃ e) ∧ stamp g n⇩1 = stamp g n⇩2) ⟶ n⇩1 = n⇩2"
    assume "n⇩1 ∈ true_ids g'"
    assume "n⇩2 ∈ true_ids g'"
    show "g' ⊢ n⇩1 ≃ e ⟹ g' ⊢ n⇩2 ≃ e ⟹ stamp g' n⇩1 = stamp g' n⇩2 ⟹ n⇩1 = n⇩2" 
    proof (cases "n⇩1 ∈ true_ids g")
      case n1: True
      then show "g' ⊢ n⇩1 ≃ e ⟹ g' ⊢ n⇩2 ≃ e ⟹ stamp g' n⇩1 = stamp g' n⇩2 ⟹ n⇩1 = n⇩2"
      proof (cases "n⇩2 ∈ true_ids g")
        case n2: True
        assume n1rep': "g' ⊢ n⇩1 ≃ e"
        assume n2rep': "g' ⊢ n⇩2 ≃ e"
        assume "stamp g' n⇩1 = stamp g' n⇩2"
        have n1rep: "g ⊢ n⇩1 ≃ e"
          using n1rep' kind_eq stamp_eq new_def add_preserves_rep
          using IRGraph.true_ids_def assms(6) n1 unchanged by auto
        have n2rep: "g ⊢ n⇩2 ≃ e"
          using n2rep' kind_eq stamp_eq new_def add_preserves_rep
          using IRGraph.true_ids_def assms(6) n2 unchanged by auto
        have "stamp g n⇩1 = stamp g n⇩2"
          by (metis ‹stamp g' n⇩1 = stamp g' n⇩2› assms(4) fresh_node_subset n1rep n2rep new subset_stamp)
        then show ?thesis using 1
          using n1 n2
          using n1rep n2rep by blast
      next
        case n2: False
        assume n1rep': "g' ⊢ n⇩1 ≃ e"
        assume n2rep': "g' ⊢ n⇩2 ≃ e"
        assume "stamp g' n⇩1 = stamp g' n⇩2"
        have "n⇩2 = n"
          using ‹n⇩2 ∈ true_ids g'› dom n2 by auto
        then have ne: "n⇩2 ∉ ids g"
          using new n2 by blast
        then show ?thesis sorry
        have n1rep: "g ⊢ n⇩1 ≃ e"
          using n1rep' kind_eq stamp_eq new_def add_preserves_rep
          by (metis DiffD1 assms(6) n1 true_ids unchanged)
        have n2rep: "g ⊢ n⇩2 ≃ e"
          using n2rep' kind_eq stamp_eq new_def add_preserves_rep
          sorry ―‹thought this seemed a bit too good to be true›
        then show "n⇩1 = n⇩2" sorry
      qed
    next
      case n1: False
      then show "g' ⊢ n⇩1 ≃ e ⟹ g' ⊢ n⇩2 ≃ e ⟹ stamp g' n⇩1 = stamp g' n⇩2 ⟹ n⇩1 = n⇩2"
      proof (cases "n⇩2 ∈ true_ids g")
        case n2: True
        assume n1rep': "g' ⊢ n⇩1 ≃ e"
        assume n2rep': "g' ⊢ n⇩2 ≃ e"
        assume "stamp g' n⇩1 = stamp g' n⇩2"
        have "n⇩1 = n"
          using ‹n⇩1 ∈ true_ids g'› dom n1 by auto
        then have ne: "n⇩1 ∉ ids g"
          using new n2 by blast
        have n1rep: "g ⊢ n⇩1 ≃ e"
          using n1rep' kind_eq stamp_eq new_def add_preserves_rep
          using ConstantNodeNew.prems(1) IRGraph.true_ids_def n1 unchanged
          by (smt (verit, best) ConstantNodeE ConstantNodeNew.hyps(1) ConstantNodeNew.hyps(3) IRNode.disc(2703) TreeToGraphThms.true_ids_def UnE ‹kind g' n = ConstantNode c› ‹n⇩1 ∈ true_ids g'› ‹stamp g' n⇩1 = stamp g' n⇩2› dom find_new_stamp find_none mem_Collect_eq n2 n2rep' rep_constant singletonD)
        then show ?thesis
          using n1rep not_in_no_rep ne by blast
      next
        case n2: False
        assume n1rep': "g' ⊢ n⇩1 ≃ e"
        assume n2rep': "g' ⊢ n⇩2 ≃ e"
        assume "stamp g' n⇩1 = stamp g' n⇩2"
        have "n⇩1 = n ∧ n⇩2 = n"
          using ‹n⇩1 ∈ true_ids g'› dom n1
          using ‹n⇩2 ∈ true_ids g'› n2 by blast
        then show ?thesis
          by simp
      qed
    qed
*)

lemma unary_inputs:
  assumes "kind g n = unary_node op x"
  shows "inputs g n = {x}"
  by (cases op; auto simp add: assms)

lemma unary_succ:
  assumes "kind g n = unary_node op x"
  shows "succ g n = {}"
  by (cases op; auto simp add: assms)

lemma binary_inputs:
  assumes "kind g n = bin_node op x y"
  shows "inputs g n = {x, y}"
  by (cases op; auto simp add: assms)

lemma binary_succ:
  assumes "kind g n = bin_node op x y"
  shows "succ g n = {}"
  by (cases op; auto simp add: assms)

lemma unrep_contains:
  assumes "g ⊕ e ↝ (g', n)"
  shows "n ∈ ids g'"
  using assms not_in_no_rep term_graph_reconstruction by blast

lemma unrep_preserves_contains:
  assumes "n ∈ ids g"
  assumes "g ⊕ e ↝ (g', n')"
  shows "n ∈ ids g'"
  by (meson subsetD unrep_ids_subset assms)

lemma unique_preserves_closure:
  assumes "wf_closed g"
  assumes "unique g (node, s) (g', n)"
  assumes "set (inputs_of node) ⊆ ids g ∧
      set (successors_of node) ⊆ ids g ∧
      node ≠ NoNode"
  shows "wf_closed g'"
  using assms
  by (smt (verit, del_insts) Pair_inject UnE add_changed fresh_ids graph_refinement_def ids_add_update inputs.simps other_node_unchanged singletonD subset_refines subset_trans succ.simps unique.cases unique_kind unique_subset wf_closed_def)


lemma unrep_preserves_closure:
  assumes "wf_closed g"
  assumes "g ⊕ e ↝ (g', n)"
  shows "wf_closed g'"
  using assms(2,1) wf_closed_def
  proof (induction g e "(g', n)" arbitrary: g' n)
  next
    case (UnrepConstantNode g c g' n)
    then show ?case using unique_preserves_closure
      by (metis IRNode.distinct(1077) IRNodes.inputs_of_ConstantNode IRNodes.successors_of_ConstantNode empty_subsetI list.set(1))
  next
    case (UnrepParameterNode g i s n)
    then show ?case using unique_preserves_closure
      by (metis IRNode.distinct(3695) IRNodes.inputs_of_ParameterNode IRNodes.successors_of_ParameterNode empty_subsetI list.set(1))
  next
    case (UnrepConditionalNode g ce g⇩1 c te g⇩2 t fe g⇩3 f s' g⇩4 n)
    then have c: "wf_closed g⇩3"
      by fastforce
    have k: "kind g⇩4 n = ConditionalNode c t f"
      using UnrepConditionalNode IRNode.distinct(965) unique_kind by presburger
    have "{c, t, f} ⊆ ids g⇩4" using unrep_contains
      by (metis UnrepConditionalNode.hyps(1) UnrepConditionalNode.hyps(3) UnrepConditionalNode.hyps(5) UnrepConditionalNode.hyps(8) empty_subsetI graph_refinement_def insert_subsetI subset_iff subset_refines unique_subset unrep_ids_subset)
    also have "inputs g⇩4 n = {c, t, f} ∧ succ g⇩4 n = {}"
      using k by simp
    moreover have "inputs g⇩4 n ⊆ ids g⇩4 ∧ succ g⇩4 n ⊆ ids g⇩4 ∧ kind g⇩4 n ≠ NoNode"
      using k
      by (metis IRNode.distinct(965) calculation empty_subsetI)
    ultimately show ?case using c unique_preserves_closure UnrepConditionalNode
      by (metis empty_subsetI inputs.simps insert_subsetI k succ.simps unrep_contains unrep_preserves_contains)
  next
    case (UnrepUnaryNode g xe g⇩1 x s' op g⇩2 n)
    then have c: "wf_closed g⇩1"
      by fastforce
    have k: "kind g⇩2 n = unary_node op x"
      using UnrepUnaryNode unique_kind unary_node_nonode by blast
    have "{x} ⊆ ids g⇩2" using unrep_contains
      by (metis UnrepUnaryNode.hyps(1) UnrepUnaryNode.hyps(4) encodes_contains ids_some singletonD subsetI term_graph_reconstruction unique_eval)
    also have "inputs g⇩2 n = {x} ∧ succ g⇩2 n = {}"
      using k
      by (meson unary_inputs unary_succ)
    moreover have "inputs g⇩2 n ⊆ ids g⇩2 ∧ succ g⇩2 n ⊆ ids g⇩2 ∧ kind g⇩2 n ≠ NoNode"
      using k
      by (metis calculation(1) calculation(2) empty_subsetI unary_node_nonode)
    ultimately show ?case using c unique_preserves_closure UnrepUnaryNode
      by (metis empty_subsetI inputs.simps insert_subsetI k succ.simps unrep_contains)
  next
    case (UnrepBinaryNode g xe g⇩1 x ye g⇩2 y s' op g⇩3 n)
    then have c: "wf_closed g⇩2"
      by fastforce
    have k: "kind g⇩3 n = bin_node op x y"
      using UnrepBinaryNode unique_kind bin_node_nonode by blast
    have "{x, y} ⊆ ids g⇩3" using unrep_contains
      by (metis UnrepBinaryNode.hyps(1) UnrepBinaryNode.hyps(3) UnrepBinaryNode.hyps(6) empty_subsetI graph_refinement_def insert_absorb insert_subset subset_refines unique_subset unrep_refines)
    also have "inputs g⇩3 n = {x, y} ∧ succ g⇩3 n = {}"
      using k
      by (meson binary_inputs binary_succ)
    moreover have "inputs g⇩3 n ⊆ ids g⇩3 ∧ succ g⇩3 n ⊆ ids g⇩3 ∧ kind g⇩3 n ≠ NoNode"
      using k
      by (metis calculation(1) calculation(2) empty_subsetI bin_node_nonode)
    ultimately show ?case using c unique_preserves_closure UnrepBinaryNode
      by (metis empty_subsetI inputs.simps insert_subsetI k succ.simps unrep_contains unrep_preserves_contains)
  next
    case (AllLeafNodes g n s)
    then show ?case
      by simp
  qed

inductive_cases ConstUnrepE: "g ⊕ (ConstantExpr x) ↝ (g', n)"

definition constant_value where
  "constant_value = (IntVal 32 0)"
definition bad_graph where
  "bad_graph = irgraph [
    (0, AbsNode 1, constantAsStamp constant_value),
    (1, RefNode 2, constantAsStamp constant_value),
    (2, ConstantNode constant_value, constantAsStamp constant_value)
  ]"

(*
experiment begin
lemma
  assumes "maximal_sharing g"
  assumes "wf_closed g"
  assumes "kind g y = AbsNode y'"
  assumes "kind g y' = RefNode y''"
  assumes "kind g y'' = ConstantNode v"
  assumes "stamp g y'' = constantAsStamp v"
  assumes "g ⊕ (UnaryExpr UnaryAbs (ConstantExpr v)) ↝ (g', n)" (is "g ⊕ ?e ↝ (g', n)")
  shows "¬(maximal_sharing g')"
  using assms(3,2,1)
proof -
  have "y'' ∈ ids g"
    using assms(5) by simp
  then have "List.member (sorted_list_of_set (ids g)) y''"
    by (metis member_def unwrap_sorted)
  then have "find (λi. kind g i = ConstantNode v ∧ stamp g i = constantAsStamp v) (sorted_list_of_set (ids g)) = Some y''"
    using assms(5,6) find_Some_iff sorry
  then have "g ⊕ ConstantExpr v ↝ (g, y'')"
    using assms(5) ConstUnrepE sorry
  then show ?thesis sorry
qed
end

lemma conditional_rep_kind:
  assumes "g ⊢ n ≃ ConditionalExpr ce te fe"
  assumes "g ⊢ c ≃ ce"
  assumes "g ⊢ t ≃ te"
  assumes "g ⊢ f ≃ fe"
  assumes "¬(∃n'. kind g n = RefNode n')"
  shows "kind g n = ConditionalNode c t f"
  using assms apply (induction n "ConditionalExpr ce te fe" rule: rep.induct) defer
  apply meson using repDet sorry

lemma unary_rep_kind:
  assumes "g ⊢ n ≃ UnaryExpr op xe"
  assumes "g ⊢ x ≃ xe"
  assumes "¬(∃n'. kind g n = RefNode n')"
  shows "kind g n = unary_node op x"
  using assms apply (cases op) using AbsNodeE sorry

lemma binary_rep_kind:
  assumes "g ⊢ n ≃ BinaryExpr op xe ye"
  assumes "g ⊢ x ≃ xe"
  assumes "g ⊢ y ≃ ye"
  assumes "¬(∃n'. kind g n = RefNode n')"
  shows "kind g n = bin_node op x y"
  using assms sorry

theorem unrep_maximal_sharing:
  assumes "maximal_sharing g"
  assumes "wf_closed g"
  assumes "g ⊕ e ↝ (g', n)"
  shows "maximal_sharing g'"
  using assms(3,2,1)
  proof (induction g e "(g', n)" arbitrary: g' n)
    case (ConstantNodeSame g c n)
    then show ?case by blast
  next
    case (ConstantNodeNew g c n g')
    then have "kind g' n = ConstantNode c"
      using find_new_kind by blast
    then have repn: "g' ⊢ n ≃ ConstantExpr c"
      using rep.ConstantNode by simp
    from ConstantNodeNew have real_node: "¬(is_RefNode (ConstantNode c)) ∧ ConstantNode c ≠ NoNode"
      by simp                       
    then have dom: "true_ids g' = true_ids g ∪ {n}"
      using ConstantNodeNew.hyps(2) ConstantNodeNew.hyps(3) fresh_ids
      by (meson true_ids_add_update)
    have new: "n ∉ ids g"
      using fresh_ids
      using ConstantNodeNew.hyps(2) by blast
    obtain new where "new = true_ids g' - true_ids g"
      by simp
    then have new_def: "new = {n}"
      by (metis (no_types, lifting) DiffE Diff_cancel IRGraph.true_ids_def Un_insert_right dom insert_Diff_if new sup_bot_right)
    then have unchanged: "(new ⊴ as_set g') = as_set g"
      using ConstantNodeNew(3) new add_node_as_set_eq
      by presburger
    then have kind_eq: "∀n' . n' ∉ new ⟶ kind g n' = kind g' n'"
      by (metis ConstantNodeNew.hyps(3) ‹new = {n}› add_node_as_set dual_order.eq_iff not_excluded_keep_type not_in_g)
    from unchanged have stamp_eq: "∀n' ∈ ids g . n' ∉ new ⟶ stamp g n' = stamp g' n'"
      using not_excluded_keep_type new_def new
      by (metis ConstantNodeNew.hyps(3) add_node_as_set)
    show ?case unfolding maximal_sharing apply (rule allI; rule allI; rule impI)
      using ConstantNodeNew(5) unfolding maximal_sharing apply auto
      proof -
      fix n⇩1 n⇩2 e
      assume 1: "∀n⇩1 n⇩2.
          n⇩1 ∈ true_ids g ∧ n⇩2 ∈ true_ids g ⟶
          (∃e. (g ⊢ n⇩1 ≃ e) ∧ (g ⊢ n⇩2 ≃ e) ∧ stamp g n⇩1 = stamp g n⇩2) ⟶ n⇩1 = n⇩2"
      assume "n⇩1 ∈ true_ids g'"
      assume "n⇩2 ∈ true_ids g'"
      show "g' ⊢ n⇩1 ≃ e ⟹ g' ⊢ n⇩2 ≃ e ⟹ stamp g' n⇩1 = stamp g' n⇩2 ⟹ n⇩1 = n⇩2" 
      proof (cases "n⇩1 ∈ true_ids g")
        case n1: True
        then show "g' ⊢ n⇩1 ≃ e ⟹ g' ⊢ n⇩2 ≃ e ⟹ stamp g' n⇩1 = stamp g' n⇩2 ⟹ n⇩1 = n⇩2"
        proof (cases "n⇩2 ∈ true_ids g")
          case n2: True
          assume n1rep': "g' ⊢ n⇩1 ≃ e"
          assume n2rep': "g' ⊢ n⇩2 ≃ e"
          assume stmp: "stamp g' n⇩1 = stamp g' n⇩2"
          have n1rep: "g ⊢ n⇩1 ≃ e"
            using n1rep' kind_eq stamp_eq new_def add_preserves_rep
            using ConstantNodeNew.prems(1) IRGraph.true_ids_def n1 unchanged by auto
          have n2rep: "g ⊢ n⇩2 ≃ e"
            using n2rep' kind_eq stamp_eq new_def add_preserves_rep
            using ConstantNodeNew.prems(1) IRGraph.true_ids_def n2 unchanged by auto
          have "stamp g n⇩1 = stamp g n⇩2"
            by (metis ConstantNodeNew.hyps(3) stmp fresh_node_subset n1rep n2rep new subset_stamp)
          then show ?thesis using 1
            using n1 n2
            using n1rep n2rep by blast
        next
          case n2: False
          assume n1rep': "g' ⊢ n⇩1 ≃ e"
          assume n2rep': "g' ⊢ n⇩2 ≃ e"
          assume stmp: "stamp g' n⇩1 = stamp g' n⇩2"
          have n2_def: "n⇩2 = n"
            using ‹n⇩2 ∈ true_ids g'› dom n2 by auto
          have n1rep: "g ⊢ n⇩1 ≃ ConstantExpr c"
            by (metis (no_types, lifting) ConstantNodeNew.prems(1) DiffE IRGraph.true_ids_def add_preserves_rep n1 n1rep' n2_def n2rep' repDet repn unchanged)
          then have n1in: "n⇩1 ∈ ids g"
            using no_encoding by metis
          have k: "kind g n⇩1 = ConstantNode c"
            using TreeToGraphThms.true_ids_def n1 n1rep by force
          have s: "stamp g n⇩1 = constantAsStamp c"
            by (metis ConstantNodeNew.hyps(3) real_node n2_def stmp find_new_stamp fresh_node_subset n1rep new subset_stamp)
          from k s show ?thesis
             using find_none ConstantNodeNew.hyps(1) n1in by blast
        qed
      next
        case n1: False
        then show "g' ⊢ n⇩1 ≃ e ⟹ g' ⊢ n⇩2 ≃ e ⟹ stamp g' n⇩1 = stamp g' n⇩2 ⟹ n⇩1 = n⇩2"
        proof (cases "n⇩2 ∈ true_ids g")
          case n2: True
          assume n1rep': "g' ⊢ n⇩1 ≃ e"
          assume n2rep': "g' ⊢ n⇩2 ≃ e"
          assume stmp: "stamp g' n⇩1 = stamp g' n⇩2"
          have n1_def: "n⇩1 = n"
            using ‹n⇩1 ∈ true_ids g'› dom n1 by auto
          have n2in: "n⇩2 ∈ ids g"
            using IRGraph.true_ids_def n2 by auto
          have k: "kind g n⇩2 = ConstantNode c"
            by (metis (mono_tags, lifting) ConstantNodeE ConstantNodeNew.prems(1) DiffE IRGraph.true_ids_def add_preserves_rep mem_Collect_eq n1_def n1rep' n2 n2rep' repDet repn unchanged)
          have s: "stamp g n⇩2 = constantAsStamp c"
            by (metis ConstantNodeNew.hyps(3) TreeToGraphThms.new_def add_node_lookup n1_def n2in real_node stamp_eq stmp unchanged)
          from k s show ?thesis
            using find_none ConstantNodeNew.hyps(1) n2in by blast
        next
          case n2: False
          assume n1rep': "g' ⊢ n⇩1 ≃ e"
          assume n2rep': "g' ⊢ n⇩2 ≃ e"
          assume "stamp g' n⇩1 = stamp g' n⇩2"
          have "n⇩1 = n ∧ n⇩2 = n"
            using ‹n⇩1 ∈ true_ids g'› dom n1
            using ‹n⇩2 ∈ true_ids g'› n2 by blast
          then show ?thesis
            by simp
        qed
      qed
    qed
  next
    case (ParameterNodeSame g i s n)
    then show ?case by blast
  next
    case (ParameterNodeNew g i s n g')
    then have k: "kind g' n = ParameterNode i"
      using find_new_kind by blast
    have "stamp g' n = s"
      using ParameterNodeNew.hyps(3) find_new_stamp by blast
    then have repn: "g' ⊢ n ≃ ParameterExpr i s"
      using rep.ParameterNode k by simp
    from ConstantNodeNew have "¬(is_RefNode (ParameterNode i)) ∧ ParameterNode i ≠ NoNode"
      by simp
    then have dom: "true_ids g' = true_ids g ∪ {n}"
      using ParameterNodeNew.hyps(2) ParameterNodeNew.hyps(3) fresh_ids
      by (meson true_ids_add_update)
    have new: "n ∉ ids g"
      using fresh_ids
      using ParameterNodeNew.hyps(2) by blast
    obtain new where "new = true_ids g' - true_ids g"
      by simp
    then have new_def: "new = {n}"
      by (metis (no_types, lifting) DiffE Diff_cancel IRGraph.true_ids_def Un_insert_right dom insert_Diff_if new sup_bot_right)
    then have unchanged: "(new ⊴ as_set g') = as_set g"
      using ParameterNodeNew(3) new add_node_as_set_eq
      by presburger
    then have kind_eq: "∀n' . n' ∉ new ⟶ kind g n' = kind g' n'"
      by (metis ParameterNodeNew.hyps(3) ‹new = {n}› add_node_as_set dual_order.eq_iff not_excluded_keep_type not_in_g)
    from unchanged have stamp_eq: "∀n' ∈ ids g . n' ∉ new ⟶ stamp g n' = stamp g' n'"
      using not_excluded_keep_type new_def new
      by (metis ParameterNodeNew.hyps(3) add_node_as_set)
    show ?case unfolding maximal_sharing apply (rule allI; rule allI; rule impI)
      using ParameterNodeNew(5) unfolding maximal_sharing apply auto
      proof -
      fix n⇩1 n⇩2 e
      assume 1: "∀n⇩1 n⇩2.
          n⇩1 ∈ true_ids g ∧ n⇩2 ∈ true_ids g ⟶
          (∃e. (g ⊢ n⇩1 ≃ e) ∧ (g ⊢ n⇩2 ≃ e) ∧ stamp g n⇩1 = stamp g n⇩2) ⟶ n⇩1 = n⇩2"
      assume "n⇩1 ∈ true_ids g'"
      assume "n⇩2 ∈ true_ids g'"
      show "g' ⊢ n⇩1 ≃ e ⟹ g' ⊢ n⇩2 ≃ e ⟹ stamp g' n⇩1 = stamp g' n⇩2 ⟹ n⇩1 = n⇩2" 
      proof (cases "n⇩1 ∈ true_ids g")
        case n1: True
        then show "g' ⊢ n⇩1 ≃ e ⟹ g' ⊢ n⇩2 ≃ e ⟹ stamp g' n⇩1 = stamp g' n⇩2 ⟹ n⇩1 = n⇩2"
        proof (cases "n⇩2 ∈ true_ids g")
          case n2: True
          assume n1rep': "g' ⊢ n⇩1 ≃ e"
          assume n2rep': "g' ⊢ n⇩2 ≃ e"
          assume "stamp g' n⇩1 = stamp g' n⇩2"
          have n1rep: "g ⊢ n⇩1 ≃ e"
            using n1rep' kind_eq stamp_eq new_def add_preserves_rep
            using ParameterNodeNew.prems(1) IRGraph.true_ids_def n1 unchanged by auto
          have n2rep: "g ⊢ n⇩2 ≃ e"
            using n2rep' kind_eq stamp_eq new_def add_preserves_rep
            using ParameterNodeNew.prems(1) IRGraph.true_ids_def n2 unchanged by auto
          have "stamp g n⇩1 = stamp g n⇩2"
            by (metis ParameterNodeNew.hyps(3) ‹stamp g' n⇩1 = stamp g' n⇩2› fresh_node_subset n1rep n2rep new subset_stamp)
          then show ?thesis using 1
            using n1 n2
            using n1rep n2rep by blast
        next
          case n2: False
          assume n1rep': "g' ⊢ n⇩1 ≃ e"
          assume n2rep': "g' ⊢ n⇩2 ≃ e"
          assume "stamp g' n⇩1 = stamp g' n⇩2"
          have "n⇩2 = n"
            using ‹n⇩2 ∈ true_ids g'› dom n2 by auto
          then have ne: "n⇩2 ∉ ids g"
            using new n2 by blast
          have n1rep: "g ⊢ n⇩1 ≃ e"
            using n1rep' kind_eq stamp_eq new_def add_preserves_rep
            using ParameterNodeNew.prems(1) IRGraph.true_ids_def n1 unchanged by auto
          have n2rep: "g ⊢ n⇩2 ≃ e"
            using n2rep' kind_eq stamp_eq new_def add_preserves_rep
            using ParameterNodeNew.prems(1) IRGraph.true_ids_def unchanged
            by (metis (no_types, lifting) IRNode.disc(2703) ParameterNodeE ParameterNodeNew.hyps(1) TreeToGraphThms.true_ids_def ‹n⇩2 = n› find_none mem_Collect_eq n1 n1rep' repDet repn)
          then show ?thesis
            using n2rep not_in_no_rep ne by blast 
        qed
      next
        case n1: False
        then show "g' ⊢ n⇩1 ≃ e ⟹ g' ⊢ n⇩2 ≃ e ⟹ stamp g' n⇩1 = stamp g' n⇩2 ⟹ n⇩1 = n⇩2"
        proof (cases "n⇩2 ∈ true_ids g")
          case n2: True
          assume n1rep': "g' ⊢ n⇩1 ≃ e"
          assume n2rep': "g' ⊢ n⇩2 ≃ e"
          assume "stamp g' n⇩1 = stamp g' n⇩2"
          have "n⇩1 = n"
            using ‹n⇩1 ∈ true_ids g'› dom n1 by auto
          then have ne: "n⇩1 ∉ ids g"
            using new n2 by blast
          have n1rep: "g ⊢ n⇩1 ≃ e"
            using n1rep' kind_eq stamp_eq new_def add_preserves_rep
            using ParameterNodeNew.prems(1) IRGraph.true_ids_def n1 unchanged
            by (metis (no_types, lifting) IRNode.disc(2703) ParameterNodeE ParameterNodeNew.hyps(1) TreeToGraphThms.true_ids_def ‹n⇩1 = n› find_none mem_Collect_eq n2 n2rep' repDet repn)
          then show ?thesis
            using n1rep not_in_no_rep ne by blast
        next
          case n2: False
          assume n1rep': "g' ⊢ n⇩1 ≃ e"
          assume n2rep': "g' ⊢ n⇩2 ≃ e"
          assume "stamp g' n⇩1 = stamp g' n⇩2"
          have "n⇩1 = n ∧ n⇩2 = n"
            using ‹n⇩1 ∈ true_ids g'› dom n1
            using ‹n⇩2 ∈ true_ids g'› n2 by blast
          then show ?thesis
            by simp
        qed
      qed
    qed
  next
    case (ConditionalNodeSame g ce g2 c te g3 t fe g4 f s' n)
    then show ?case
      using unrep_preserves_closure by blast
  next
    case (ConditionalNodeNew g ce g2 c te g3 t fe g4 f s' n g')
    then have k: "kind g' n = ConditionalNode c t f"
      using find_new_kind by blast
    have "stamp g' n = s'"
      using ConditionalNodeNew.hyps(10) IRNode.distinct(591) find_new_stamp by blast
    then have repn: "g' ⊢ n ≃ ConditionalExpr ce te fe"
      using rep.ConditionalNode k
      by (metis ConditionalNodeNew.hyps(1) ConditionalNodeNew.hyps(10) ConditionalNodeNew.hyps(3) ConditionalNodeNew.hyps(5) ConditionalNodeNew.hyps(9) fresh_ids fresh_node_subset subset_implies_evals term_graph_reconstruction)
    from ConstantNodeNew have "¬(is_RefNode (ConditionalNode c t f)) ∧ ConditionalNode c t f ≠ NoNode"
      by simp
    then have dom: "true_ids g' = true_ids g4 ∪ {n}"
      using ConditionalNodeNew.hyps(10) ConditionalNodeNew.hyps(9) fresh_ids true_ids_add_update by presburger
    have new: "n ∉ ids g"
      using fresh_ids
      by (meson ConditionalNodeNew.hyps(1) ConditionalNodeNew.hyps(3) ConditionalNodeNew.hyps(5) ConditionalNodeNew.hyps(9) unrep_preserves_contains)
    obtain new where "new = true_ids g' - true_ids g4"
      by simp
    then have new_def: "new = {n}"
      using dom
      by (metis ConditionalNodeNew.hyps(9) DiffD1 DiffI Diff_cancel Diff_insert Un_insert_right boolean_algebra.disj_zero_right fresh_ids insertCI insert_Diff true_ids)
    then have unchanged: "(new ⊴ as_set g') = as_set g4"
      using new add_node_as_set_eq
      using ConditionalNodeNew.hyps(10) ConditionalNodeNew.hyps(9) fresh_ids by presburger
    then have kind_eq: "∀n' . n' ∉ new ⟶ kind g4 n' = kind g' n'"
      by (metis ConditionalNodeNew.hyps(10) add_node_as_set equalityE local.new_def not_excluded_keep_type not_in_g)
    from unchanged have stamp_eq: "∀n' ∈ ids g . n' ∉ new ⟶ stamp g4 n' = stamp g' n'"
      using not_excluded_keep_type new_def new
      by (metis ConditionalNodeNew.hyps(1) ConditionalNodeNew.hyps(10) ConditionalNodeNew.hyps(3) ConditionalNodeNew.hyps(5) add_node_as_set unrep_preserves_contains)
    have max_g4: "maximal_sharing g4"
      using ConditionalNodeNew.hyps(1) ConditionalNodeNew.hyps(2) ConditionalNodeNew.hyps(3) ConditionalNodeNew.hyps(4) ConditionalNodeNew.hyps(6) ConditionalNodeNew.prems(1) ConditionalNodeNew.prems(2) unrep_preserves_closure by blast
    show ?case unfolding maximal_sharing apply (rule allI; rule allI; rule impI)
      using max_g4 unfolding maximal_sharing apply auto
      proof -
      fix n⇩1 n⇩2 e
      assume 1: "∀n⇩1 n⇩2.
          n⇩1 ∈ true_ids g4 ∧ n⇩2 ∈ true_ids g4 ⟶
          (∃e. (g4 ⊢ n⇩1 ≃ e) ∧ (g4 ⊢ n⇩2 ≃ e) ∧ stamp g4 n⇩1 = stamp g4 n⇩2) ⟶ n⇩1 = n⇩2"
      assume "n⇩1 ∈ true_ids g'"
      assume "n⇩2 ∈ true_ids g'"
      show "g' ⊢ n⇩1 ≃ e ⟹ g' ⊢ n⇩2 ≃ e ⟹ stamp g' n⇩1 = stamp g' n⇩2 ⟹ n⇩1 = n⇩2" 
      proof (cases "n⇩1 ∈ true_ids g4")
        case n1: True
        then show "g' ⊢ n⇩1 ≃ e ⟹ g' ⊢ n⇩2 ≃ e ⟹ stamp g' n⇩1 = stamp g' n⇩2 ⟹ n⇩1 = n⇩2"
        proof (cases "n⇩2 ∈ true_ids g4")
          case n2: True
          assume n1rep': "g' ⊢ n⇩1 ≃ e"
          assume n2rep': "g' ⊢ n⇩2 ≃ e"
          assume "stamp g' n⇩1 = stamp g' n⇩2"
          have n1rep: "g4 ⊢ n⇩1 ≃ e"
            using n1rep' kind_eq stamp_eq new_def add_preserves_rep
            using ConditionalNodeNew.prems(1) IRGraph.true_ids_def n1 unchanged
            by (metis (mono_tags, lifting) ConditionalNodeNew.hyps(1) ConditionalNodeNew.hyps(3) ConditionalNodeNew.hyps(5) DiffE unrep_preserves_closure)
          have n2rep: "g4 ⊢ n⇩2 ≃ e"
            using n2rep' kind_eq stamp_eq new_def add_preserves_rep
            using ConditionalNodeNew.prems(1) IRGraph.true_ids_def n2 unchanged
            by (metis (no_types, lifting) ConditionalNodeNew.hyps(1) ConditionalNodeNew.hyps(3) ConditionalNodeNew.hyps(5) DiffE unrep_preserves_closure)
          have "stamp g4 n⇩1 = stamp g4 n⇩2"
            by (metis ConditionalNodeNew.hyps(10) ConditionalNodeNew.hyps(9) ‹stamp g' n⇩1 = stamp g' n⇩2› fresh_ids fresh_node_subset n1rep n2rep subset_stamp)
          then show ?thesis using 1
            using n1 n2
            using n1rep n2rep by blast
        next
          case n2: False
          assume n1rep': "g' ⊢ n⇩1 ≃ e"
          assume n2rep': "g' ⊢ n⇩2 ≃ e"
          assume stmp: "stamp g' n⇩1 = stamp g' n⇩2"
          have n2_def: "n⇩2 = n"
            using ‹n⇩2 ∈ true_ids g'› dom n2 by auto
          have n1rep: "g4 ⊢ n⇩1 ≃ ConditionalExpr ce te fe"
            by (metis (no_types, lifting) ConditionalNodeNew.hyps(1) ConditionalNodeNew.hyps(3) ConditionalNodeNew.hyps(5) ConditionalNodeNew.prems(1) Diff_iff IRGraph.true_ids_def add_preserves_rep n1 n1rep' n2_def n2rep' repDet repn unchanged unrep_preserves_closure)
          then have n1in: "n⇩1 ∈ ids g4"
            using no_encoding by metis
          (*have inputs_true: "c ∈ true_ids g4 ∧ t ∈ true_ids g4 ∧ f ∈ true_ids g4"
            sorry
          have rep: "(g4 ⊢ c ≃ ce) ∧ (g4 ⊢ t ≃ te) ∧ (g4 ⊢ f ≃ fe)"
            by (metis ConditionalNodeNew.hyps(1) ConditionalNodeNew.hyps(3) ConditionalNodeNew.hyps(5) not_in_no_rep term_graph_reconstruction unrep_unchanged)
          have cuni: "∀n' ∈ true_ids g4. (g4 ⊢ n' ≃ ce) ∧ stamp g4 n' = stamp g4 c ⟶ n' = c"
            using max_g4 unfolding maximal_sharing using inputs_true
            by (meson local.rep)
          have tuni: "∀n' ∈ true_ids g4. (g4 ⊢ n' ≃ te) ∧ stamp g4 n' = stamp g4 t ⟶ n' = t"
            using max_g4 unfolding maximal_sharing using inputs_true
            by (meson local.rep)
          have funi: "∀n' ∈ true_ids g4. (g4 ⊢ n' ≃ fe) ∧ stamp g4 n' = stamp g4 f ⟶ n' = f"
            using max_g4 unfolding maximal_sharing using inputs_true
            by (meson local.rep)
          then obtain cx tx fx where k: "kind g4 n⇩1 = ConditionalNode cx tx fx"
            by (metis (mono_tags, lifting) ConditionalNodeE IRNode.discI(51) TreeToGraphThms.true_ids_def mem_Collect_eq n1 n1rep)
          have "c = cx"
            using cuni rep inputs_true sorry
          have s: "stamp g4 n⇩1 = s'"
            by (metis ConditionalNodeNew.hyps(10) ConditionalNodeNew.hyps(9) ‹stamp g' n = s'› fresh_ids fresh_node_subset n1rep n2_def stmp subset_stamp)*)
          have rep: "(g4 ⊢ c ≃ ce) ∧ (g4 ⊢ t ≃ te) ∧ (g4 ⊢ f ≃ fe)"
            by (meson ConditionalNodeNew.hyps(1) ConditionalNodeNew.hyps(3) ConditionalNodeNew.hyps(5) subset_implies_evals term_graph_reconstruction)
          have not_ref: "¬(∃n'. kind g4 n⇩1 = RefNode n')"
            using TreeToGraphThms.true_ids_def n1 by fastforce
          then have "kind g4 n⇩1 = ConditionalNode c t f"
            using conditional_rep_kind
            using local.rep n1rep by presburger
          then show ?thesis
            using find_none ConditionalNodeNew.hyps(8) n1in
            by (metis ConditionalNodeNew.hyps(10) ConditionalNodeNew.hyps(9) ‹stamp g' n = s'› fresh_ids fresh_node_subset n1rep n2_def stmp subset_stamp)
        qed
      next
        case n1: False
        then show "g' ⊢ n⇩1 ≃ e ⟹ g' ⊢ n⇩2 ≃ e ⟹ stamp g' n⇩1 = stamp g' n⇩2 ⟹ n⇩1 = n⇩2"
        proof (cases "n⇩2 ∈ true_ids g4")
          case n2: True
          assume n1rep': "g' ⊢ n⇩1 ≃ e"
          assume n2rep': "g' ⊢ n⇩2 ≃ e"
          assume "stamp g' n⇩1 = stamp g' n⇩2"
          have new_n1: "n⇩1 = n"
            using ‹n⇩1 ∈ true_ids g'› dom n1 by auto
          then have ne: "n⇩1 ∉ ids g4"
            using new n1
            using ConditionalNodeNew.hyps(9) fresh_ids by blast
          have unrep_cond: "g4 ⊢ n⇩2 ≃ ConditionalExpr ce te fe"
            using n1rep' kind_eq stamp_eq new_def add_preserves_rep
            using ConditionalNodeNew.prems(1) IRGraph.true_ids_def n2 unchanged
            by (metis (no_types, lifting) ConditionalNodeNew.hyps(1) ConditionalNodeNew.hyps(3) ConditionalNodeNew.hyps(5) DiffD1 n2rep' new_n1 repDet repn unrep_preserves_closure)
          have rep: "(g4 ⊢ c ≃ ce) ∧ (g4 ⊢ t ≃ te) ∧ (g4 ⊢ f ≃ fe)"
            by (meson ConditionalNodeNew.hyps(1) ConditionalNodeNew.hyps(3) ConditionalNodeNew.hyps(5) subset_implies_evals term_graph_reconstruction)
          have not_ref: "¬(∃n'. kind g4 n⇩2 = RefNode n')"
            using TreeToGraphThms.true_ids_def n2 by fastforce
          then have "kind g4 n⇩2 = ConditionalNode c t f"
            using conditional_rep_kind
            using local.rep unrep_cond by presburger
          then show ?thesis using find_none ConditionalNodeNew.hyps(8)
            by (metis ConditionalNodeNew.hyps(10) ‹stamp g' n = s'› ‹stamp g' n⇩1 = stamp g' n⇩2› encodes_contains fresh_node_subset ne new_n1 not_in_g subset_stamp unrep_cond)
        next
          case n2: False
          assume n1rep': "g' ⊢ n⇩1 ≃ e"
          assume n2rep': "g' ⊢ n⇩2 ≃ e"
          assume "stamp g' n⇩1 = stamp g' n⇩2"
          have "n⇩1 = n ∧ n⇩2 = n"
            using ‹n⇩1 ∈ true_ids g'› dom n1
            using ‹n⇩2 ∈ true_ids g'› n2
            by simp
          then show ?thesis
            by simp
        qed
      qed
    qed
  next
    case (UnaryNodeSame g xe g2 x s' op n)
    then show ?case by blast
  next
    case (UnaryNodeNew g xe g2 x s' op n g')
    then have k: "kind g' n = unary_node op x"
      using find_new_kind
      by (metis add_node_lookup fresh_ids ids_some)
    have "stamp g' n = s'"
      by (metis UnaryNodeNew.hyps(6) empty_iff find_new_stamp ids_some insertI1 k not_in_g_inputs unary_inputs)
    then have repn: "g' ⊢ n ≃ UnaryExpr op xe"
      using k
      using UnaryNodeNew.hyps(1) UnaryNodeNew.hyps(3) UnaryNodeNew.hyps(4) UnaryNodeNew.hyps(5) UnaryNodeNew.hyps(6) term_graph_reconstruction unrep.UnaryNodeNew by blast
    from ConstantNodeNew have "¬(is_RefNode (unary_node op x)) ∧ unary_node op x ≠ NoNode"
      by (cases op; auto)
    then have dom: "true_ids g' = true_ids g2 ∪ {n}"
      using UnaryNodeNew.hyps(5) UnaryNodeNew.hyps(6) fresh_ids true_ids_add_update by presburger
    have new: "n ∉ ids g"
      using fresh_ids
      by (meson UnaryNodeNew.hyps(1) UnaryNodeNew.hyps(5) unrep_preserves_contains)
    obtain new where "new = true_ids g' - true_ids g2"
      by simp
    then have new_def: "new = {n}"
      using dom
      by (metis Diff_cancel Diff_iff Un_insert_right UnaryNodeNew.hyps(5) fresh_ids insert_Diff_if sup_bot.right_neutral true_ids)
    then have unchanged: "(new ⊴ as_set g') = as_set g2"
      using new add_node_as_set_eq
      using UnaryNodeNew.hyps(5) UnaryNodeNew.hyps(6) fresh_ids by presburger
    then have kind_eq: "∀n' . n' ∉ new ⟶ kind g2 n' = kind g' n'"
      by (metis UnaryNodeNew.hyps(6) add_node_as_set equalityD1 local.new_def not_excluded_keep_type not_in_g)
    from unchanged have stamp_eq: "∀n' ∈ ids g . n' ∉ new ⟶ stamp g2 n' = stamp g' n'"
      using not_excluded_keep_type new_def new
      by (metis UnaryNodeNew.hyps(1) UnaryNodeNew.hyps(6) add_node_as_set unrep_preserves_contains)
    have max_g2: "maximal_sharing g2"
      by (simp add: UnaryNodeNew.hyps(2) UnaryNodeNew.prems(1) UnaryNodeNew.prems(2))
    show ?case unfolding maximal_sharing apply (rule allI; rule allI; rule impI)
      using max_g2 unfolding maximal_sharing apply auto
      proof -
      fix n⇩1 n⇩2 e
      assume 1: "∀n⇩1 n⇩2.
          n⇩1 ∈ true_ids g2 ∧ n⇩2 ∈ true_ids g2 ⟶
          (∃e. (g2 ⊢ n⇩1 ≃ e) ∧ (g2 ⊢ n⇩2 ≃ e) ∧ stamp g2 n⇩1 = stamp g2 n⇩2) ⟶ n⇩1 = n⇩2"
      assume "n⇩1 ∈ true_ids g'"
      assume "n⇩2 ∈ true_ids g'"
      show "g' ⊢ n⇩1 ≃ e ⟹ g' ⊢ n⇩2 ≃ e ⟹ stamp g' n⇩1 = stamp g' n⇩2 ⟹ n⇩1 = n⇩2" 
      proof (cases "n⇩1 ∈ true_ids g2")
        case n1: True
        then show "g' ⊢ n⇩1 ≃ e ⟹ g' ⊢ n⇩2 ≃ e ⟹ stamp g' n⇩1 = stamp g' n⇩2 ⟹ n⇩1 = n⇩2"
        proof (cases "n⇩2 ∈ true_ids g2")
          case n2: True
          assume n1rep': "g' ⊢ n⇩1 ≃ e"
          assume n2rep': "g' ⊢ n⇩2 ≃ e"
          assume "stamp g' n⇩1 = stamp g' n⇩2"
          have n1rep: "g2 ⊢ n⇩1 ≃ e"
            using n1rep' kind_eq stamp_eq new_def add_preserves_rep
            using Diff_iff IRGraph.true_ids_def UnaryNodeNew.hyps(1) UnaryNodeNew.prems(1) n1 unchanged unrep_preserves_closure by auto
          have n2rep: "g2 ⊢ n⇩2 ≃ e"
            using n2rep' kind_eq stamp_eq new_def add_preserves_rep
            by (metis (no_types, lifting) Diff_iff IRGraph.true_ids_def UnaryNodeNew.hyps(1) UnaryNodeNew.prems(1) n2 unchanged unrep_preserves_closure)
          have "stamp g2 n⇩1 = stamp g2 n⇩2"
            by (metis UnaryNodeNew.hyps(5) UnaryNodeNew.hyps(6) ‹stamp g' n⇩1 = stamp g' n⇩2› fresh_ids fresh_node_subset n1rep n2rep subset_stamp)
          then show ?thesis using 1
            using n1 n2
            using n1rep n2rep by blast
        next
          case n2: False
          assume n1rep': "g' ⊢ n⇩1 ≃ e"
          assume n2rep': "g' ⊢ n⇩2 ≃ e"
          assume "stamp g' n⇩1 = stamp g' n⇩2"
          have new_n2: "n⇩2 = n"
            using ‹n⇩2 ∈ true_ids g'› dom n2 by auto
          then have ne: "n⇩2 ∉ ids g2"
            using new n2
            using UnaryNodeNew.hyps(5) fresh_ids by blast
          have unrep_un: "g2 ⊢ n⇩1 ≃ UnaryExpr op xe"
            using n1rep' kind_eq stamp_eq new_def add_preserves_rep
            by (metis (no_types, lifting) Diff_iff IRGraph.true_ids_def UnaryNodeNew.hyps(1) UnaryNodeNew.prems(1) n1 n2rep' new_n2 repDet repn unchanged unrep_preserves_closure)
          have rep: "(g2 ⊢ x ≃ xe)"
            using UnaryNodeNew.hyps(1) term_graph_reconstruction by auto
          have not_ref: "¬(∃n'. kind g2 n⇩1 = RefNode n')"
            using TreeToGraphThms.true_ids_def n1 by force
          then have "kind g2 n⇩1 = unary_node op x"
            using unrep_un unary_rep_kind rep by simp
            (*apply (frule ConditionalNodeE[where ?g = g4 and ?n = n⇩1 and ?ce = ce and ?te = te and ?fe = fe])*)
          then show ?thesis using find_none UnaryNodeNew.hyps(4)
            by (metis UnaryNodeNew.hyps(6) ‹stamp g' n = s'› ‹stamp g' n⇩1 = stamp g' n⇩2› fresh_node_subset ne new_n2 no_encoding subset_stamp unrep_un)
        qed
      next
        case n1: False
        then show "g' ⊢ n⇩1 ≃ e ⟹ g' ⊢ n⇩2 ≃ e ⟹ stamp g' n⇩1 = stamp g' n⇩2 ⟹ n⇩1 = n⇩2"
        proof (cases "n⇩2 ∈ true_ids g2")
          case n2: True
          assume n1rep': "g' ⊢ n⇩1 ≃ e"
          assume n2rep': "g' ⊢ n⇩2 ≃ e"
          assume "stamp g' n⇩1 = stamp g' n⇩2"
          have new_n1: "n⇩1 = n"
            using ‹n⇩1 ∈ true_ids g'› dom n1 by auto
          then have ne: "n⇩1 ∉ ids g2"
            using new n1
            using UnaryNodeNew.hyps(5) fresh_ids by blast
          have unrep_un: "g2 ⊢ n⇩2 ≃ UnaryExpr op xe"
            using n1rep' kind_eq stamp_eq new_def add_preserves_rep
            by (metis (no_types, lifting) Diff_iff IRGraph.true_ids_def UnaryNodeNew.hyps(1) UnaryNodeNew.prems(1) n2 n2rep' new_n1 repDet repn unchanged unrep_preserves_closure)
          have rep: "(g2 ⊢ x ≃ xe)"
            using UnaryNodeNew.hyps(1) term_graph_reconstruction by presburger
          have not_ref: "¬(∃n'. kind g2 n⇩2 = RefNode n')"
            using TreeToGraphThms.true_ids_def n2 by fastforce
          then have "kind g2 n⇩2 = unary_node op x"
            using unary_rep_kind
            using local.rep unrep_un by presburger
          then show ?thesis using find_none UnaryNodeNew.hyps(4)
            by (metis UnaryNodeNew.hyps(6) ‹stamp g' n = s'› ‹stamp g' n⇩1 = stamp g' n⇩2› fresh_node_subset ne new_n1 no_encoding subset_stamp unrep_un)
        next
          case n2: False
          assume n1rep': "g' ⊢ n⇩1 ≃ e"
          assume n2rep': "g' ⊢ n⇩2 ≃ e"
          assume "stamp g' n⇩1 = stamp g' n⇩2"
          have "n⇩1 = n ∧ n⇩2 = n"
            using ‹n⇩1 ∈ true_ids g'› dom n1
            using ‹n⇩2 ∈ true_ids g'› n2
            by simp
          then show ?thesis
            by simp
        qed
      qed
    qed
  next
    case (BinaryNodeSame g xe g2 x ye g3 y s' op n)
    then show ?case
      using unrep_preserves_closure by blast
  next
    case (BinaryNodeNew g xe g2 x ye g3 y s' op n g')
    then have k: "kind g' n = bin_node op x y"
      using find_new_kind
      by (metis add_node_lookup fresh_ids ids_some)
    have "stamp g' n = s'"
      by (metis BinaryNodeNew.hyps(1) BinaryNodeNew.hyps(3) BinaryNodeNew.hyps(5) BinaryNodeNew.hyps(6) BinaryNodeNew.hyps(7) BinaryNodeNew.hyps(8) find_new_stamp ids_some k unrep.BinaryNodeNew unrep_contains)
    then have repn: "g' ⊢ n ≃ BinaryExpr op xe ye"
      using k
      using BinaryNodeNew.hyps(1) BinaryNodeNew.hyps(3) BinaryNodeNew.hyps(5) BinaryNodeNew.hyps(6) BinaryNodeNew.hyps(7) BinaryNodeNew.hyps(8) term_graph_reconstruction unrep.BinaryNodeNew by blast
    from BinaryNodeNew have "¬(is_RefNode (bin_node op x y)) ∧ bin_node op x y ≠ NoNode"
      by (cases op; auto) (* slow *)
    then have dom: "true_ids g' = true_ids g3 ∪ {n}"
      using BinaryNodeNew.hyps(7) BinaryNodeNew.hyps(8) fresh_ids true_ids_add_update by presburger
    have new: "n ∉ ids g"
      using fresh_ids
      by (meson BinaryNodeNew.hyps(1) BinaryNodeNew.hyps(3) BinaryNodeNew.hyps(7) unrep_preserves_contains)
    obtain new where "new = true_ids g' - true_ids g3"
      by simp
    then have new_def: "new = {n}"
      using dom
      by (metis BinaryNodeNew.hyps(7) Diff_cancel Diff_iff Un_insert_right fresh_ids insert_Diff_if sup_bot.right_neutral true_ids)
    then have unchanged: "(new ⊴ as_set g') = as_set g3"
      using new add_node_as_set_eq
      using BinaryNodeNew.hyps(7) BinaryNodeNew.hyps(8) fresh_ids by presburger
    then have kind_eq: "∀n' . n' ∉ new ⟶ kind g3 n' = kind g' n'"
      by (metis BinaryNodeNew.hyps(8) add_node_as_set equalityD1 local.new_def not_excluded_keep_type not_in_g)
    from unchanged have stamp_eq: "∀n' ∈ ids g . n' ∉ new ⟶ stamp g3 n' = stamp g' n'"
      using not_excluded_keep_type new_def new
      by (metis BinaryNodeNew.hyps(1) BinaryNodeNew.hyps(3) BinaryNodeNew.hyps(8) add_node_as_set unrep_preserves_contains)
    have max_g3: "maximal_sharing g3"
      using BinaryNodeNew.hyps(1) BinaryNodeNew.hyps(2) BinaryNodeNew.hyps(4) BinaryNodeNew.prems(1) BinaryNodeNew.prems(2) unrep_preserves_closure by blast
    show ?case unfolding maximal_sharing apply (rule allI; rule allI; rule impI)
      using max_g3 unfolding maximal_sharing apply auto
      proof -
      fix n⇩1 n⇩2 e
      assume 1: "∀n⇩1 n⇩2.
          n⇩1 ∈ true_ids g3 ∧ n⇩2 ∈ true_ids g3 ⟶
          (∃e. (g3 ⊢ n⇩1 ≃ e) ∧ (g3 ⊢ n⇩2 ≃ e) ∧ stamp g3 n⇩1 = stamp g3 n⇩2) ⟶ n⇩1 = n⇩2"
      assume "n⇩1 ∈ true_ids g'"
      assume "n⇩2 ∈ true_ids g'"
      show "g' ⊢ n⇩1 ≃ e ⟹ g' ⊢ n⇩2 ≃ e ⟹ stamp g' n⇩1 = stamp g' n⇩2 ⟹ n⇩1 = n⇩2" 
      proof (cases "n⇩1 ∈ true_ids g3")
        case n1: True
        then show "g' ⊢ n⇩1 ≃ e ⟹ g' ⊢ n⇩2 ≃ e ⟹ stamp g' n⇩1 = stamp g' n⇩2 ⟹ n⇩1 = n⇩2"
        proof (cases "n⇩2 ∈ true_ids g3")
          case n2: True
          assume n1rep': "g' ⊢ n⇩1 ≃ e"
          assume n2rep': "g' ⊢ n⇩2 ≃ e"
          assume "stamp g' n⇩1 = stamp g' n⇩2"
          have n1rep: "g3 ⊢ n⇩1 ≃ e"
            using n1rep' kind_eq stamp_eq new_def add_preserves_rep
            by (metis (no_types, lifting) BinaryNodeNew.hyps(1) BinaryNodeNew.hyps(3) BinaryNodeNew.prems(1) Diff_iff IRGraph.true_ids_def n1 unchanged unrep_preserves_closure)
          have n2rep: "g3 ⊢ n⇩2 ≃ e"
            using n2rep' kind_eq stamp_eq new_def add_preserves_rep
            by (metis BinaryNodeNew.hyps(1) BinaryNodeNew.hyps(3) BinaryNodeNew.prems(1) DiffE n2 true_ids unchanged unrep_preserves_closure)
          have "stamp g3 n⇩1 = stamp g3 n⇩2"
            by (metis BinaryNodeNew.hyps(7) BinaryNodeNew.hyps(8) ‹stamp g' n⇩1 = stamp g' n⇩2› fresh_ids fresh_node_subset n1rep n2rep subset_stamp)
          then show ?thesis using 1
            using n1 n2
            using n1rep n2rep by blast
        next
          case n2: False
          assume n1rep': "g' ⊢ n⇩1 ≃ e"
          assume n2rep': "g' ⊢ n⇩2 ≃ e"
          assume "stamp g' n⇩1 = stamp g' n⇩2"
          have new_n2: "n⇩2 = n"
            using ‹n⇩2 ∈ true_ids g'› dom n2 by auto
          then have ne: "n⇩2 ∉ ids g3"
            using new n2
            using BinaryNodeNew.hyps(7) fresh_ids by presburger
          have unrep_bin: "g3 ⊢ n⇩1 ≃ BinaryExpr op xe ye"
            using n1rep' kind_eq stamp_eq new_def add_preserves_rep
            by (metis BinaryNodeNew.hyps(1) BinaryNodeNew.hyps(3) BinaryNodeNew.prems(1) DiffE ‹new = true_ids g' - true_ids g3› encodes_contains ids_some n1 n2rep' new_n2 repDet repn unchanged unrep_preserves_closure)
          have rep: "(g3 ⊢ x ≃ xe) ∧ (g3 ⊢ y ≃ ye)"
            by (meson BinaryNodeNew.hyps(1) BinaryNodeNew.hyps(3) term_graph_reconstruction unrep_contains unrep_unchanged)
          have not_ref: "¬(∃n'. kind g3 n⇩1 = RefNode n')"
            using TreeToGraphThms.true_ids_def n1 by force
          then have "kind g3 n⇩1 = bin_node op x y"
            using unrep_bin binary_rep_kind rep by simp
          then show ?thesis using find_none BinaryNodeNew.hyps(6)
            by (metis BinaryNodeNew.hyps(8) ‹stamp g' n = s'› ‹stamp g' n⇩1 = stamp g' n⇩2› fresh_node_subset ne new_n2 no_encoding subset_stamp unrep_bin)
        qed
      next
        case n1: False
        then show "g' ⊢ n⇩1 ≃ e ⟹ g' ⊢ n⇩2 ≃ e ⟹ stamp g' n⇩1 = stamp g' n⇩2 ⟹ n⇩1 = n⇩2"
        proof (cases "n⇩2 ∈ true_ids g3")
          case n2: True
          assume n1rep': "g' ⊢ n⇩1 ≃ e"
          assume n2rep': "g' ⊢ n⇩2 ≃ e"
          assume "stamp g' n⇩1 = stamp g' n⇩2"
          have new_n1: "n⇩1 = n"
            using ‹n⇩1 ∈ true_ids g'› dom n1 by auto
          then have ne: "n⇩1 ∉ ids g3"
            using new n1
            using BinaryNodeNew.hyps(7) fresh_ids by blast
          have unrep_bin: "g3 ⊢ n⇩2 ≃ BinaryExpr op xe ye"
            using n1rep' kind_eq stamp_eq new_def add_preserves_rep
            by (metis (mono_tags, lifting) BinaryNodeNew.hyps(1) BinaryNodeNew.hyps(3) BinaryNodeNew.prems(1) Diff_iff IRGraph.true_ids_def n2 n2rep' new_n1 repDet repn unchanged unrep_preserves_closure)
          have rep: "(g3 ⊢ x ≃ xe) ∧ (g3 ⊢ y ≃ ye)"
            using BinaryNodeNew.hyps(1) BinaryNodeNew.hyps(3) term_graph_reconstruction unrep_contains unrep_unchanged by blast
          have not_ref: "¬(∃n'. kind g3 n⇩2 = RefNode n')"
            using TreeToGraphThms.true_ids_def n2 by fastforce
          then have "kind g3 n⇩2 = bin_node op x y"
            using unrep_bin binary_rep_kind rep by simp
          then show ?thesis using find_none BinaryNodeNew.hyps(6)
            by (metis BinaryNodeNew.hyps(8) ‹stamp g' n = s'› ‹stamp g' n⇩1 = stamp g' n⇩2› fresh_node_subset ne new_n1 no_encoding subset_stamp unrep_bin)
        next
          case n2: False
          assume n1rep': "g' ⊢ n⇩1 ≃ e"
          assume n2rep': "g' ⊢ n⇩2 ≃ e"
          assume "stamp g' n⇩1 = stamp g' n⇩2"
          have "n⇩1 = n ∧ n⇩2 = n"
            using ‹n⇩1 ∈ true_ids g'› dom n1
            using ‹n⇩2 ∈ true_ids g'› n2
            by simp
          then show ?thesis
            by simp
        qed
      qed
    qed
  next
    case (AllLeafNodes g n s)
    then show ?case by blast
  qed
*)

end