1 files changed, 43 insertions, 4 deletions

diff --git a/HoTT_Methods.thy b/HoTT_Methods.thy
index 20f3ece..81e2055 100644
--- a/HoTT_Methods.thy
+++ b/HoTT_Methods.thy
@@ -10,6 +10,7 @@ theory HoTT_Methods
     "HOL-Eisbach.Eisbach"
     "HOL-Eisbach.Eisbach_Tools"
     HoTT_Base
+    Prod
 begin
 
 
@@ -19,17 +20,17 @@ text "Prove type judgments \<open>A : U\<close> and inhabitation judgments \<ope
 
 Can also perform typechecking, and search for elements of a type."
 
-method simple uses lems = (assumption|standard|rule lems)+
+method simple uses lems = (assumption | standard | rule lems)+
 
 
 text "Find a proof of any valid typing judgment derivable from a given wellformed judgment."
 
-method wellformed uses jdgmt = (
+\<comment> \<open>\<open>wellform\<close> is declared in HoTT_Base.thy\<close>
+method wellformed uses jdgmt declares wellform =
   match wellform in rl: "PROP ?P" \<Rightarrow> \<open>(
     catch \<open>rule rl[OF jdgmt]\<close> \<open>fail\<close> |
     catch \<open>wellformed jdgmt: rl[OF jdgmt]\<close> \<open>fail\<close>
     )\<close>
-  )
 
 
 text "Combine \<open>simple\<close> and \<open>wellformed\<close> to search for derivations.
@@ -45,7 +46,45 @@ method derive uses lems unfolds = (
   )+
 
 
-text "Simplify function applications."
+text "Simplify a function application."
+
+method simplify for expr::Term uses lems = match (expr) in
+  "(\<^bold>\<lambda>x:?A. ?b x)`?a" \<Rightarrow> \<open>
+    print_term "Single application",
+    rule Prod_comp,
+    derive lems: lems
+    \<close> \<bar>
+  "(F`a)`b" for F a b \<Rightarrow> \<open>
+    print_term "Repeated application",
+    simplify "F`a"
+    \<close>
+  
+
+
+text "Verify a function application simplification."
+
+method verify_simp uses lems = (
+  print_term "Attempting simplification",
+  ( rule comp | derive lems: lems | simp add: lems )+
+  | print_fact lems,
+    match conclusion in
+    "F`a`b \<equiv> x" for F a b x \<Rightarrow> \<open>
+      print_term "Chained application",
+      print_term F,
+      print_term a,
+      print_term b,
+      print_term x,
+      match (F) in
+        "\<^bold>\<lambda>x:A. f x" for A f \<Rightarrow> \<open>
+          print_term "Matched abstraction",
+          print_fact Prod_comp[where ?A = A and ?b = f and ?a = a]
+          \<close> \<bar>
+        "?x" \<Rightarrow> \<open>
+          print_term "Constant application",
+          print_fact comp
+          \<close>
+      \<close>
+  )
 
 
 end
\ No newline at end of file